let Y, X be set ; :: thesis: ( Y <> {} implies rng (pr1 X,Y) = X )
assume A1: Y <> {} ; :: thesis: rng (pr1 X,Y) = X
consider y being Element of Y;
A2: rng (pr1 X,Y) c= X by Th59;
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 x in X ; :: thesis: x in rng (pr1 X,Y)
then ( [x,y] in [:X,Y:] & (pr1 X,Y) . x,y = x ) by A1, Def5, ZFMISC_1:106;
then ( [x,y] in dom (pr1 X,Y) & (pr1 X,Y) . x,y = x ) by Def5;
hence x in rng (pr1 X,Y) by FUNCT_1:def 5; :: thesis: verum

end;

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