proposition: Lemma AdjointUA_comp_law : Fcomp_law AdjointUA_map.
proof: Proof. unfold Fcomp_law in |- *; simpl in |- *. unfold AdjointUA_mor, AdjointUA_ob in |- *; intros d1 d2 d3 f g. apply UA_unic1. apply Trans with (UA_mor (UA_of d1) o FMor G (UA_diese (UA_of d1) (f o UA_mor (UA_of d2))) o FMor G (UA_diese (UA_of d2) (g o UA_mor (UA_of d3)))). apply Comp_l; apply FComp. apply Trans with ((UA_mor (UA_of d1) o FMor G (UA_diese (UA_of d1) (f o UA_mor (UA_of d2)))) o FMor G (UA_diese (UA_of d2) (g o UA_mor (UA_of d3)))). apply Ass. apply Trans with ((f o UA_mor (UA_of d2)) o FMor G (UA_diese (UA_of d2) (g o UA_mor (UA_of d3)))). apply Comp_r; apply UA_diag. apply Trans with (f o UA_mor (UA_of d2) o FMor G (UA_diese (UA_of d2) (g o UA_mor (UA_of d3)))). apply Ass1. apply Trans with (f o g o UA_mor (UA_of d3)). apply Comp_l; apply UA_diag. apply Ass. Qed.
imports: Adj_UA