let f be Function; :: thesis: ( f = {} implies f " = {} )
assume f = {} ; :: thesis: f " = {}
then dom (f ") = {} by FUNCT_1:33, RELAT_1:38;
hence f " = {} ; :: thesis: verum