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