set A = { o where o is Element of F_{1}() : P_{1}[o] } ;

_{2}() = { o where o is Element of F_{1}() : P_{1}[o] }
by XTUPLE_0:def 12; :: thesis: verum

now :: thesis: for x being object holds

( ( x in { o where o is Element of F_{1}() : P_{1}[o] } implies ex y being object st [x,y] in F_{2}() ) & ( ex y being object st [x,y] in F_{2}() implies x in { o where o is Element of F_{1}() : P_{1}[o] } ) )

hence
dom F( ( x in { o where o is Element of F

let x be object ; :: thesis: ( ( x in { o where o is Element of F_{1}() : P_{1}[o] } implies ex y being object st [x,y] in F_{2}() ) & ( ex y being object st [x,y] in F_{2}() implies x in { o where o is Element of F_{1}() : P_{1}[o] } ) )

_{2}()
; :: thesis: x in { o where o is Element of F_{1}() : P_{1}[o] }

consider o being Element of F_{1}() such that

A4: [x,y] = [o,F_{3}(o)]
and

A5: P_{1}[o]
by A1, A3;

x = o by A4, XTUPLE_0:1;

hence x in { o where o is Element of F_{1}() : P_{1}[o] }
by A5; :: thesis: verum

end;hereby :: thesis: ( ex y being object st [x,y] in F_{2}() implies x in { o where o is Element of F_{1}() : P_{1}[o] } )

given y being object such that A3:
[x,y] in Fassume
x in { o where o is Element of F_{1}() : P_{1}[o] }
; :: thesis: ex y being object st [x,y] in F_{2}()

then consider o being Element of F_{1}() such that

A2: ( x = o & P_{1}[o] )
;

reconsider y = F_{3}(o) as object ;

take y = y; :: thesis: [x,y] in F_{2}()

thus [x,y] in F_{2}()
by A1, A2; :: thesis: verum

end;then consider o being Element of F

A2: ( x = o & P

reconsider y = F

take y = y; :: thesis: [x,y] in F

thus [x,y] in F

consider o being Element of F

A4: [x,y] = [o,F

A5: P

x = o by A4, XTUPLE_0:1;

hence x in { o where o is Element of F