f in Ob C ;
then consider f1 being morphism of C such that
A1: ( f = f1 & f1 is identity & f1 in Mor C ) ;
( F . f1 is identity & F . f1 in Mor D ) by A1, Def22, Def25;
then F . f1 in Ob D ;
hence F . f is Object of D by A1, Def21; :: thesis: verum