proposition: Lemma CoadjointUA_map_law : Map_law CoadjointUA_mor.
proof: Proof. unfold Map_law, CoadjointUA_mor in |- *; intros f g H. apply (Codiese_map (UA_of c') (x:=CoUA_mor (UA_of c) o f) (y:=CoUA_mor (UA_of c) o g)). apply Comp_l; assumption. Qed.
imports: Adj_UA