per cases ( not Mor D is empty or Mor D is empty ) ;

suppose not Mor D is empty ; :: thesis: ex b₁ being Functor of C,D st b₁ 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;

suppose C is empty ; :: thesis: F . f is identity

then F . f is Object of D1 by Def21;
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 b₁ being Functor of C,D st b₁ 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;