let X, Y be set ; :: thesis: ( X <> {} implies rng (pr2 X,Y) = Y )
consider x being Element of X;
assume A1: X <> {} ; :: thesis: rng (pr2 X,Y) = Y
A2: Y c= rng (pr2 X,Y)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in rng (pr2 X,Y) )
assume A3: y in Y ; :: thesis: y in rng (pr2 X,Y)
then [x,y] in [:X,Y:] by A1, ZFMISC_1:106;
then A4: [x,y] in dom (pr2 X,Y) by Def6;
(pr2 X,Y) . x,y = y by A1, A3, Def6;
hence y in rng (pr2 X,Y) by A4, FUNCT_1:def 5; :: thesis: verum

end;

rng (pr2 X,Y) c= Y by Th61;
hence rng (pr2 X,Y) = Y by A2, XBOOLE_0:def 10; :: thesis: verum