let f be Function; :: thesis:
assume not f is constant ; :: thesis:
then consider n1, n2 being object such that
A1: n1 in dom f and
A2: n2 in dom f and
A3: f . n1 <> f . n2 ;
reconsider f = f as non empty Function by A1;
not f is trivial

reconsider x = [n1,(f . n1)], y = [n2,(f . n2)] as Element of f by A1, A2, Th1;
take x ; :: according to ZFMISC_1:def 10 :: thesis:
take y ; :: thesis:
thus ( x in f & y in f ) ; :: thesis:
thus not x = y by A3, XTUPLE_0:1; :: thesis:

end;