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