per cases ( f is empty or f <> {} ) ;
suppose f is empty ; :: thesis: rng f is trivial
then reconsider g = f as empty Function ;
rng g is empty ;
hence rng f is trivial ; :: thesis: verum
end;
suppose f <> {} ; :: thesis: rng f is trivial
then consider x being object such that
A1: x in dom f by XBOOLE_0:def 1;
for y being object holds
( y in {(f . x)} iff ex z being object st
( z in dom f & y = f . z ) )
proof
let y be object ; :: thesis: ( y in {(f . x)} iff ex z being object st
( z in dom f & y = f . z ) )
hereby :: thesis: ( ex z being object st
( z in dom f & y = f . z ) implies y in {(f . x)} )
assume A2: y in {(f . x)} ; :: thesis: ex x being object st
( x in dom f & y = f . x )
reconsider x = x as object ;
take x = x; :: thesis: ( x in dom f & y = f . x )
thus ( x in dom f & y = f . x ) by A1, A2, TARSKI:def 1; :: thesis: verum
end;
given z being object such that A3: ( z in dom f & y = f . z ) ; :: thesis: y in {(f . x)}
y = f . x by A1, A3, Def10;
hence y in {(f . x)} by TARSKI:def 1; :: thesis: verum
end;
hence rng f is trivial by Def3; :: thesis: verum
end;
end;