thus ( not C is empty implies F . f is morphism of D ) :: thesis: ( ( C is empty implies the Object of D is morphism of D ) & ( for b₁ being morphism of D holds verum ) )

proof

assume A1: not C is empty ; :: thesis: F . f is morphism of D

per cases ( Mor D <> {} or Mor D = {} ) ;

suppose Mor D <> {} ; :: thesis: F . f is morphism of D

hence F . f is morphism of D by A1, FUNCT_2:5; :: thesis: verum

end;

suppose Mor D = {} ; :: thesis: F . f is morphism of D

hence F . f is morphism of D by SUBSET_1:def 1; :: thesis: verum

end;

end;

end;

the Object of D is morphism of D

proof

per cases ( Mor D <> {} or Mor D = {} ) ;

suppose Mor D <> {} ; :: thesis: the Object of D is morphism of D

then not D is empty ;
hence the Object of D is morphism of D by TARSKI:def 3; :: thesis: verum

end;

suppose Mor D = {} ; :: thesis: the Object of D is morphism of D

hence the Object of D is morphism of D ; :: thesis: verum

end;

end;

end;

hence ( ( C is empty implies the Object of D is morphism of D ) & ( for b₁ being morphism of D holds verum ) ) ; :: thesis: verum