set A = { o where o is Element of F1() : P1[o] } ;
now :: thesis: 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 ; :: thesis: ( ( 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 :: thesis: ( 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] } ; :: thesis: 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; :: thesis: [x,y] in F2()
thus [x,y] in F2() by A1, A2; :: thesis: verum
end;
given y being object such that A3: [x,y] in F2() ; :: thesis: 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 ;
hence x in { o where o is Element of F1() : P1[o] } by A5; :: thesis: verum
end;
hence dom F2() = { o where o is Element of F1() : P1[o] } by XTUPLE_0:def 12; :: thesis: verum