let A be Subset of [:NAT,NAT:]; proj2 A = { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A }
set A2 = { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } ;
A1:
proj2 A c= { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A }
proof
let y be
object ;
TARSKI:def 3 ( not y in proj2 A or y in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } )
assume
y in proj2 A
;
y in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A }
then consider x being
object such that A2:
[x,y] in A
by XTUPLE_0:def 13;
ex
x1,
y1 being
object st
(
x1 in NAT &
y1 in NAT &
[x,y] = [x1,y1] )
by A2, ZFMISC_1:def 2;
then reconsider x =
x,
y =
y as
Element of
NAT by XTUPLE_0:1;
(
[x,y] in A &
y is
Element of
NAT )
by A2;
hence
y in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A }
;
verum
end;
{ y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } c= proj2 A
hence
proj2 A = { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A }
by A1; verum