let X, Y be set ; :: thesis: ( Y <> {} implies rng (pr1 (X,Y)) = X )
set y = the Element of Y;
assume A1: Y <> {} ; :: thesis: rng (pr1 (X,Y)) = X
A2: X c= rng (pr1 (X,Y))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in rng (pr1 (X,Y)) )
assume A3: x in X ; :: thesis: x in rng (pr1 (X,Y))
then [x, the Element of Y] in [:X,Y:] by A1, ZFMISC_1:87;
then A4: [x, the Element of Y] in dom (pr1 (X,Y)) by Def4;
(pr1 (X,Y)) . (x, the Element of Y) = x by A1, A3, Def4;
hence x in rng (pr1 (X,Y)) by A4, FUNCT_1:def 3; :: thesis: verum

end;

rng (pr1 (X,Y)) c= X by Th43;
hence rng (pr1 (X,Y)) = X by A2, XBOOLE_0:def 10; :: thesis: verum