let X, Y be set ; :: thesis: rng (pr1 (X,Y)) c= X
let x be object ; :: 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 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; :: thesis: verum