let C be CategoryStr ; :: thesis: for f being morphism of C st C is empty holds
f is identity
let f be morphism of C; :: thesis: ( C is empty implies f is identity )
assume C is empty ; :: thesis: f is identity
then ( ( for f1 being morphism of C st f |> f1 holds
f (*) f1 = f1 ) & ( for f1 being morphism of C st f1 |> f holds
f1 (*) f = f1 ) ) ;
then ( f is left_identity & f is right_identity ) ;
hence f is identity ; :: thesis: verum