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