let f be Function; :: thesis: ( not f is constant implies not f is trivial )
assume not f is constant ; :: thesis: not f is trivial
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

proof

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: ex b₁ being object st
( x in f & b₁ in f & not x = b₁ )
take y ; :: thesis: ( x in f & y in f & not x = y )
thus ( x in f & y in f ) ; :: thesis: not x = y
thus not x = y by A3, XTUPLE_0:1; :: thesis: verum

end;

hence not f is trivial ; :: thesis: verum