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