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;