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