set A = { o where o is Element of F1() : P1[o] } ;
now for x being object holds
( ( x in { o where o is Element of F1() : P1[o] } implies ex y being object st [x,y] in F2() ) & ( ex y being object st [x,y] in F2() implies x in { o where o is Element of F1() : P1[o] } ) )let x be
object ;
( ( x in { o where o is Element of F1() : P1[o] } implies ex y being object st [x,y] in F2() ) & ( ex y being object st [x,y] in F2() implies x in { o where o is Element of F1() : P1[o] } ) )hereby ( ex y being object st [x,y] in F2() implies x in { o where o is Element of F1() : P1[o] } )
assume
x in { o where o is Element of F1() : P1[o] }
;
ex y being object st [x,y] in F2()then consider o being
Element of
F1()
such that A2:
(
x = o &
P1[
o] )
;
reconsider y =
F3(
o) as
object ;
take y =
y;
[x,y] in F2()thus
[x,y] in F2()
by A1, A2;
verum
end; given y being
object such that A3:
[x,y] in F2()
;
x in { o where o is Element of F1() : P1[o] } consider o being
Element of
F1()
such that A4:
[x,y] = [o,F3(o)]
and A5:
P1[
o]
by A1, A3;
x = o
by A4, XTUPLE_0:1;
hence
x in { o where o is Element of F1() : P1[o] }
by A5;
verum end;
hence
dom F2() = { o where o is Element of F1() : P1[o] }
by XTUPLE_0:def 12; verum