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₁()
then A7: F₂(a) c= F₁() by A2;
c . a = F₂(a) by A6, A5;
hence c . a in bool F₁() by A7; :: 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 A c= c . A

proof

let A be Subset of F₁(); :: thesis: A c= c . A
c . A = F₂(A) by A5;
hence A c= 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;

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