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 b1 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
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 b1 being morphism of D holds verum ) ) ; :: thesis: verum