let X, Y be set ; :: thesis: ( X <> {} implies rng (pr2 X,Y) = Y )
assume A1: X <> {} ; :: thesis: rng (pr2 X,Y) = Y
consider x being Element of X;
A2: rng (pr2 X,Y) c= Y by Th61;
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 y in Y ; :: thesis: y in rng (pr2 X,Y)
then ( [x,y] in [:X,Y:] & (pr2 X,Y) . x,y = y ) by A1, Def6, ZFMISC_1:106;
then ( [x,y] in dom (pr2 X,Y) & (pr2 X,Y) . x,y = y ) by Def6;
hence y in rng (pr2 X,Y) by FUNCT_1:def 5; :: thesis: verum

end;

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