let X, Y be set ; :: thesis: rng (pr2 (X,Y)) c= Y
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (pr2 (X,Y)) or y in Y )
assume y in rng (pr2 (X,Y)) ; :: thesis: y in Y
then consider p being object such that
A1: p in dom (pr2 (X,Y)) and
A2: y = (pr2 (X,Y)) . p by FUNCT_1:def 3;
p in [:X,Y:] by A1, Def5;
then consider x1, y1 being object such that
A3: ( x1 in X & y1 in Y ) and
A4: p = [x1,y1] by ZFMISC_1:def 2;
y = (pr2 (X,Y)) . (x1,y1) by A2, A4;
hence y in Y by A3, Def5; :: thesis: verum