let g, h be Function; :: according to CARD_3:def 10 :: thesis: ( g in {f} & h in {f} implies dom g = dom h )
assume g in {f} ; :: thesis: ( not h in {f} or dom g = dom h )
then g = f by TARSKI:def 1;
hence ( not h in {f} or dom g = dom h ) by TARSKI:def 1; :: thesis: verum