let X, Y be set ; :: thesis: rng (pr2 X,Y) c= Y
let y be set ; :: 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 set such that
A1: p in dom (pr2 X,Y) and
A2: y = (pr2 X,Y) . p by FUNCT_1:def 5;
p in [:X,Y:] by A1, Def6;
then consider x1, y1 being set 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, Def6; :: thesis: verum