proposition: Lemma UA_unic1 : forall (u : UA) (a' : A) (f : b --> G a') (g : UA_ob u --> a'), UA_mor u o FMor G g =_S f -> UA_diese u f =_S g.
proof: Proof. intros u a' f g H; apply Sym; apply UA_unic; exact H. Qed.
imports: CatProperty Functor