per cases ( not Mor D is empty or Mor D is empty ) ;
suppose not Mor D is empty ; :: thesis: ex b1 being Functor of C,D st b1 is identity-preserving
then reconsider D1 = D as non empty with_identities CategoryStr ;
A1: not Ob D1 is empty ;
set F = (Mor C) --> the Object of D;
the Object of D in Ob D by A1;
then reconsider F = (Mor C) --> the Object of D as Function of C,D by FUNCOP_1:45;
take F ; :: thesis: F is identity-preserving
for f being morphism of C st f is identity holds
F . f is identity
proof
let f be morphism of C; :: thesis: ( f is identity implies F . f is identity )
assume f is identity ; :: thesis: F . f is identity
reconsider x = f as object ;
per cases ( not C is empty or C is empty ) ;
suppose A2: not C is empty ; :: thesis: F . f is identity
F . f = F . x by A2, Def21
.= the Object of D by A2, FUNCOP_1:7 ;
then F . f is Object of D1 ;
hence F . f is identity by Th22; :: thesis: verum
end;
end;
end;
hence F is identity-preserving ; :: thesis: verum
end;
suppose A3: Mor D is empty ; :: thesis: ex b1 being Functor of C,D st b1 is identity-preserving
set F = the Function of C,D;
take the Function of C,D ; :: thesis: the Function of C,D is identity-preserving
for f being morphism of C st f is identity holds
the Function of C,D . f is identity
proof
let f be morphism of C; :: thesis: ( f is identity implies the Function of C,D . f is identity )
assume f is identity ; :: thesis: the Function of C,D . f is identity
D is empty by A3;
hence the Function of C,D . f is identity by Th10; :: thesis: verum
end;
hence the Function of C,D is identity-preserving ; :: thesis: verum
end;
end;