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

proof

let x be set ; :: 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,y] in [:X,Y:] by A1, ZFMISC_1:106;
then A4: [x,y] in dom (pr1 (X,Y)) by Def5;
(pr1 (X,Y)) . (x,y) = x by A1, A3, Def5;
hence x in rng (pr1 (X,Y)) by A4, FUNCT_1:def 5; :: thesis: verum

end;

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