let X, Y be set ; ( X <> {} implies rng (pr2 (X,Y)) = Y )
set x = the Element of X;
assume A1:
X <> {}
; rng (pr2 (X,Y)) = Y
A2:
Y c= rng (pr2 (X,Y))
proof
let y be
object ;
TARSKI:def 3 ( not y in Y or y in rng (pr2 (X,Y)) )
assume A3:
y in Y
;
y in rng (pr2 (X,Y))
then
[ the Element of X,y] in [:X,Y:]
by A1, ZFMISC_1:87;
then A4:
[ the Element of X,y] in dom (pr2 (X,Y))
by Def5;
(pr2 (X,Y)) . ( the
Element of
X,
y)
= y
by A1, A3, Def5;
hence
y in rng (pr2 (X,Y))
by A4, FUNCT_1:def 3;
verum
end;
rng (pr2 (X,Y)) c= Y
by Th45;
hence
rng (pr2 (X,Y)) = Y
by A2, XBOOLE_0:def 10; verum