begin
definition
existence
ex b1 being non empty strict TopSpace st
( the carrier of b1 = product (NAT --> {0,1}) & ex P being prebasis of b1 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 ) ) )
uniqueness
for b1, b2 being non empty strict TopSpace st the carrier of b1 = product (NAT --> {0,1}) & ex P being prebasis of b1 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 b2 = product (NAT --> {0,1}) & ex P being prebasis of b2 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 ) ) holds
b1 = b2
end;