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

proof

let y be object ; :: 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 [ the Element of X,y] in [:X,Y:] by A1, ZFMISC_1:87;
then A4: [ the Element of X,y] in dom (pr2 (X,Y)) by Def5;
(pr2 (X,Y)) . ( the Element of X,y) = y by A1, A3, Def5;
hence y in rng (pr2 (X,Y)) by A4, FUNCT_1:def 3; :: thesis: verum

end;

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