proposition: Lemma CoadjointUA_comp_law : Fcomp_law CoadjointUA_map.
proof: Proof. unfold Fcomp_law in |- *; simpl in |- *. unfold CoadjointUA_mor, CoadjointUA_ob in |- *; intros c1 c2 c3 f g. apply CoUA_unic1. apply Trans with ((FMor F (CoUA_diese (UA_of c2) (CoUA_mor (UA_of c1) o f)) o FMor F (CoUA_diese (UA_of c3) (CoUA_mor (UA_of c2) o g))) o CoUA_mor (UA_of c3)). apply Comp_r; apply FComp. apply Trans with (FMor F (CoUA_diese (UA_of c2) (CoUA_mor (UA_of c1) o f)) o FMor F (CoUA_diese (UA_of c3) (CoUA_mor (UA_of c2) o g)) o CoUA_mor (UA_of c3)). apply Ass1. apply Trans with (FMor F (CoUA_diese (UA_of c2) (CoUA_mor (UA_of c1) o f)) o CoUA_mor (UA_of c2) o g). apply Comp_l; apply CoUA_diag. apply Trans with ((FMor F (CoUA_diese (UA_of c2) (CoUA_mor (UA_of c1) o f)) o CoUA_mor (UA_of c2)) o g). apply Ass. apply Trans with ((CoUA_mor (UA_of c1) o f) o g). apply Comp_r; apply CoUA_diag. apply Ass1. Qed.
imports: Adj_UA