let X, Y be set ; rng (pr1 (X,Y)) c= X
let x be object ; TARSKI:def 3 ( not x in rng (pr1 (X,Y)) or x in X )
assume
x in rng (pr1 (X,Y))
; x in X
then consider p being object such that
A1:
p in dom (pr1 (X,Y))
and
A2:
x = (pr1 (X,Y)) . p
by FUNCT_1:def 3;
p in [:X,Y:]
by A1, Def4;
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;
x = (pr1 (X,Y)) . (x1,y1)
by A2, A4;
hence
x in X
by A3, Def4; verum