set A = { o where o is Element of F₁() : P₁[o] } ;

now :: thesis: for x being object holds
( ( x in { o where o is Element of F₁() : P₁[o] } implies ex y being object st [x,y] in F₂() ) & ( ex y being object st [x,y] in F₂() implies x in { o where o is Element of F₁() : P₁[o] } ) )

let x be object ; :: thesis: ( ( x in { o where o is Element of F₁() : P₁[o] } implies ex y being object st [x,y] in F₂() ) & ( ex y being object st [x,y] in F₂() implies x in { o where o is Element of F₁() : P₁[o] } ) )

hereby :: thesis: ( ex y being object st [x,y] in F₂() implies x in { o where o is Element of F₁() : P₁[o] } )

assume x in { o where o is Element of F₁() : P₁[o] } ; :: thesis: ex y being object st [x,y] in F₂()
then consider o being Element of F₁() such that
A2: ( x = o & P₁[o] ) ;
reconsider y = F₃(o) as object ;
take y = y; :: thesis: [x,y] in F₂()
thus [x,y] in F₂() by A1, A2; :: thesis: verum

end;

given y being object such that A3: [x,y] in F₂() ; :: thesis: x in { o where o is Element of F₁() : P₁[o] }
consider o being Element of F₁() such that
A4: [x,y] = [o,F₃(o)] and
A5: P₁[o] by A1, A3;
x = o by A4, XTUPLE_0:1;
hence x in { o where o is Element of F₁() : P₁[o] } by A5; :: thesis: verum

end;

hence dom F₂() = { o where o is Element of F₁() : P₁[o] } by XTUPLE_0:def 12; :: thesis: verum