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