assume A1: rng f is trivial ; :: thesis: contradiction

per cases ( rng f is empty or not rng f is empty ) ;

suppose rng f is empty ; :: thesis: contradiction

then reconsider f = f as empty Function ;
f is trivial ;
hence contradiction ; :: thesis: verum

end;

suppose not rng f is empty ; :: thesis: contradiction

then consider x being set such that
A2: x in rng f by XBOOLE_0:def 1;
f is constant

proof

let y, z be set ; :: according to FUNCT_1:def 16 :: thesis: ( y in dom f & z in dom f implies f . y = f . z )
assume ( y in dom f & z in dom f ) ; :: thesis: f . y = f . z
then A: ( f . y in rng f & f . z in rng f ) by Def5;
hence f . y = x by A1, A2, ZFMISC_1:def 10
.= f . z by A, A1, A2, ZFMISC_1:def 10 ;
:: thesis: verum

end;

hence contradiction ; :: thesis: verum

end;

end;