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 set such that
A1: x in dom f by XBOOLE_0:def 1;
for y being set holds
( y in {(f . x)} iff ex z being set st
( z in dom f & y = f . z ) )

proof

let y be set ; :: thesis: ( y in {(f . x)} iff ex z being set st
( z in dom f & y = f . z ) )

hereby :: thesis: ( ex z being set st
( z in dom f & y = f . z ) implies y in {(f . x)} )

assume A2: y in {(f . x)} ; :: thesis: ex x being set st
( x in dom f & y = f . x )
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 set such that A3: z in dom f and
A4: y = f . z ; :: thesis: y in {(f . x)}
y = f . x by A1, A3, A4, Def16;
hence y in {(f . x)} by TARSKI:def 1; :: thesis: verum

end;

hence rng f is trivial by Def5; :: thesis: verum

end;

end;