set X = F₁();
consider c being Function such that
A5: ( dom c = bool F₁() & ( for a being set st a in bool F₁() holds
c . a = F₂(a) ) ) from FUNCT_1:sch 5();

now :: thesis: for a being object st a in bool F₁() holds
c . a in bool F₁()

let a be object ; :: thesis: ( a in bool F₁() implies c . a in bool F₁() )
assume A6: a in bool F₁() ; :: thesis: c . a in bool F₁()
reconsider aa = a as set by TARSKI:1;
A7: F₂(a) c= aa by A2, A6;
c . a = F₂(a) by A6, A5;
then c . a c= F₁() by A7, A6, XBOOLE_1:1;
hence c . a in bool F₁() ; :: thesis: verum

end;

then reconsider c = c as Function of (bool F₁()),(bool F₁()) by A5, FUNCT_2:3;
A8: for A being Subset of F₁() holds c . A c= A

proof

let A be Subset of F₁(); :: thesis: c . A c= A
c . A = F₂(A) by A5;
hence c . A c= A by A2; :: thesis: verum

end;

A9: for A, B being Subset of F₁() holds c . (A /\ B) = (c . A) /\ (c . B)

proof

let A, B be Subset of F₁(); :: thesis: c . (A /\ B) = (c . A) /\ (c . B)
A10: c . B = F₂(B) by A5;
A11: F₂((A /\ B)) = c . (A /\ B) by A5;
c . A = F₂(A) by A5;
hence c . (A /\ B) = (c . A) /\ (c . B) by A10, A11, A3; :: thesis: verum

end;

A12: for A being Subset of F₁() holds c . (c . A) = c . A

proof

let A be Subset of F₁(); :: thesis: c . (c . A) = c . A
A13: F₂((c . A)) = c . (c . A) by A5;
c . A = F₂(A) by A5;
hence c . (c . A) = c . A by A13, A4; :: thesis: verum

end;

A14: c . F₁() = F₁() by A1, A5;
then reconsider T = TopStruct(# F₁(),(rng c) #) as strict TopSpace by A12, A8, A9, Th9;
take T ; :: thesis: ( the carrier of T = F₁() & ( for A being Subset of T holds Int A = F₂(A) ) )
thus the carrier of T = F₁() ; :: thesis: for A being Subset of T holds Int A = F₂(A)
let A be Subset of T; :: thesis: Int A = F₂(A)
thus Int A = c . A by A14, A8, A9, A12, Th9
.= F₂(A) by A5 ; :: thesis: verum