set X = F1();
consider c being Function such that
A5: ( dom c = bool F1() & ( for a being set st a in bool F1() holds
c . a = F2(a) ) ) from FUNCT_1:sch 5();
now :: thesis: for a being object st a in bool F1() holds
c . a in bool F1()
let a be object ; :: thesis: ( a in bool F1() implies c . a in bool F1() )
assume A6: a in bool F1() ; :: thesis: c . a in bool F1()
then A7: F2(a) c= F1() by A2;
c . a = F2(a) by A6, A5;
hence c . a in bool F1() by A7; :: thesis: verum
end;
then reconsider c = c as Function of (bool F1()),(bool F1()) by A5, FUNCT_2:3;
A8: for A being Subset of F1() holds A c= c . A
proof
let A be Subset of F1(); :: thesis: A c= c . A
c . A = F2(A) by A5;
hence A c= c . A by A2; :: thesis: verum
end;
A9: for A, B being Subset of F1() holds c . (A \/ B) = (c . A) \/ (c . B)
proof
let A, B be Subset of F1(); :: thesis: c . (A \/ B) = (c . A) \/ (c . B)
A10: c . B = F2(B) by A5;
A11: F2((A \/ B)) = c . (A \/ B) by A5;
c . A = F2(A) by A5;
hence c . (A \/ B) = (c . A) \/ (c . B) by A10, A11, A3; :: thesis: verum
end;
A12: for A being Subset of F1() holds c . (c . A) = c . A
proof
let A be Subset of F1(); :: thesis: c . (c . A) = c . A
A13: F2((c . A)) = c . (c . A) by A5;
c . A = F2(A) by A5;
hence c . (c . A) = c . A by A13, A4; :: thesis: verum
end;
{} c= F1() ;
then A14: c . {} = {} by A1, A5;
then reconsider T = TopStruct(# F1(),(COMPLEMENT (rng c)) #) as strict TopSpace by A12, A8, A9, Th7;
take T ; :: thesis: ( the carrier of T = F1() & ( for A being Subset of T holds Cl A = F2(A) ) )
thus the carrier of T = F1() ; :: thesis: for A being Subset of T holds Cl A = F2(A)
let A be Subset of T; :: thesis: Cl A = F2(A)
thus Cl A = c . A by A14, A8, A9, A12, Th7
.= F2(A) by A5 ; :: thesis: verum