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 object such that
A2: x in rng f ;
f is constant
proof
let y, z be object ; :: according to FUNCT_1:def 10 :: thesis: ( y in dom f & z in dom f implies f . y = f . z )
assume that
A3: y in dom f and
A4: z in dom f ; :: thesis: f . y = f . z
A5: f . z in rng f by A4, Def3;
f . y in rng f by A3, Def3;
hence f . y = x by A1, A2
.= f . z by A1, A2, A5 ;
:: thesis: verum
end;
hence contradiction ; :: thesis: verum
end;
end;