set X = F_{1}();

consider c being Function such that

A5: ( dom c = bool F_{1}() & ( for a being set st a in bool F_{1}() holds

c . a = F_{2}(a) ) )
from FUNCT_1:sch 5();

_{1}()),(bool F_{1}()) by A5, FUNCT_2:3;

A8: for A being Subset of F_{1}() holds A c= c . A
_{1}() holds c . (A \/ B) = (c . A) \/ (c . B)
_{1}() holds c . (c . A) = c . A
_{1}()
;

then A14: c . {} = {} by A1, A5;

then reconsider T = TopStruct(# F_{1}(),(COMPLEMENT (rng c)) #) as strict TopSpace by A12, A8, A9, Th7;

take T ; :: thesis: ( the carrier of T = F_{1}() & ( for A being Subset of T holds Cl A = F_{2}(A) ) )

thus the carrier of T = F_{1}()
; :: thesis: for A being Subset of T holds Cl A = F_{2}(A)

let A be Subset of T; :: thesis: Cl A = F_{2}(A)

thus Cl A = c . A by A14, A8, A9, A12, Th7

.= F_{2}(A)
by A5
; :: thesis: verum

consider c being Function such that

A5: ( dom c = bool F

c . a = F

now :: thesis: for a being object st a in bool F_{1}() holds

c . a in bool F_{1}()

then reconsider c = c as Function of (bool Fc . a in bool F

let a be object ; :: thesis: ( a in bool F_{1}() implies c . a in bool F_{1}() )

assume A6: a in bool F_{1}()
; :: thesis: c . a in bool F_{1}()

then A7: F_{2}(a) c= F_{1}()
by A2;

c . a = F_{2}(a)
by A6, A5;

hence c . a in bool F_{1}()
by A7; :: thesis: verum

end;assume A6: a in bool F

then A7: F

c . a = F

hence c . a in bool F

A8: for A being Subset of F

proof

A9:
for A, B being Subset of F
let A be Subset of F_{1}(); :: thesis: A c= c . A

c . A = F_{2}(A)
by A5;

hence A c= c . A by A2; :: thesis: verum

end;c . A = F

hence A c= c . A by A2; :: thesis: verum

proof

A12:
for A being Subset of F
let A, B be Subset of F_{1}(); :: thesis: c . (A \/ B) = (c . A) \/ (c . B)

A10: c . B = F_{2}(B)
by A5;

A11: F_{2}((A \/ B)) = c . (A \/ B)
by A5;

c . A = F_{2}(A)
by A5;

hence c . (A \/ B) = (c . A) \/ (c . B) by A10, A11, A3; :: thesis: verum

end;A10: c . B = F

A11: F

c . A = F

hence c . (A \/ B) = (c . A) \/ (c . B) by A10, A11, A3; :: thesis: verum

proof

{} c= F
let A be Subset of F_{1}(); :: thesis: c . (c . A) = c . A

A13: F_{2}((c . A)) = c . (c . A)
by A5;

c . A = F_{2}(A)
by A5;

hence c . (c . A) = c . A by A13, A4; :: thesis: verum

end;A13: F

c . A = F

hence c . (c . A) = c . A by A13, A4; :: thesis: verum

then A14: c . {} = {} by A1, A5;

then reconsider T = TopStruct(# F

take T ; :: thesis: ( the carrier of T = F

thus the carrier of T = F

let A be Subset of T; :: thesis: Cl A = F

thus Cl A = c . A by A14, A8, A9, A12, Th7

.= F