let T1, T2 be non empty strict TopSpace; :: thesis: ( the carrier of T1 = product (NAT --> {0,1}) & ex P being prebasis of T1 st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) & the carrier of T2 = product (NAT --> {0,1}) & ex P being prebasis of T2 st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) implies T1 = T2 )
assume that
A2: the carrier of T1 = product (NAT --> {0,1}) and
A3: ex P being prebasis of T1 st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) and
A4: the carrier of T2 = product (NAT --> {0,1}) and
A5: ex P being prebasis of T2 st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) ; :: thesis: T1 = T2
consider P1 being prebasis of T1 such that
A6: for X being Subset of (product (NAT --> {0,1})) holds
( X in P1 iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) by A3;
consider P2 being prebasis of T2 such that
A7: for X being Subset of (product (NAT --> {0,1})) holds
( X in P2 iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) by A5;

now :: thesis: for x being Subset of (product (NAT --> {0,1})) holds
( x in P1 iff x in P2 )

let x be Subset of (product (NAT --> {0,1})); :: thesis: ( x in P1 iff x in P2 )
( x in P1 iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in x iff F . N = n ) ) by A6;
hence ( x in P1 iff x in P2 ) by A7; :: thesis: verum

end;

then P1 = P2 by A2, A4, SUBSET_1:3;
hence T1 = T2 by A2, A4, Th17; :: thesis: verum