set A = { o where o is Element of F1() : P1[o] } ;
now
let x be set ; :: thesis: ( ( x in { o where o is Element of F1() : P1[o] } implies ex y being set st [x,y] in F2() ) & ( ex y being set st [x,y] in F2() implies x in { o where o is Element of F1() : P1[o] } ) )
hereby :: thesis: ( ex y being set 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 set st [x,y] in F2()
then consider o being Element of F1() such that
A2: ( x = o & P1[o] ) ;
take y = F3(o); :: thesis: [x,y] in F2()
thus [x,y] in F2() by A1, A2; :: thesis: verum
end;
given y being set 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 A4, ZFMISC_1:27;
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 RELAT_1:def 4; :: thesis: verum