let I be 1 -element set ; for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for P being Subset of (product (Carrier J)) holds
( P in product_prebasis J iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )
let J be non-Empty TopStruct-yielding ManySortedSet of I; for i being Element of I
for P being Subset of (product (Carrier J)) holds
( P in product_prebasis J iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )
let i be Element of I; for P being Subset of (product (Carrier J)) holds
( P in product_prebasis J iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )
card I = 1
by CARD_1:def 7;
then A1:
I = {i}
by ORDERS_5:2;
the carrier of (J . i) =
[#] (J . i)
by STRUCT_0:def 3
.=
(Carrier J) . i
by PENCIL_3:7
;
then A2:
Carrier J = {i} --> the carrier of (J . i)
by A1, Th7;
let P be Subset of (product (Carrier J)); ( P in product_prebasis J iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )
hereby ( ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) implies P in product_prebasis J )
assume
P in product_prebasis J
;
ex W being Subset of (J . i) st
( W is open & P = product ({i} --> W) )then consider j being
set ,
T being
TopStruct ,
V being
Subset of
T such that A3:
(
j in I &
V is
open &
T = J . j )
and A4:
P = product ((Carrier J) +* (j,V))
by WAYBEL18:def 2;
A5:
i = j
by A1, A3, TARSKI:def 1;
reconsider W =
V as
Subset of
(J . i) by A1, A3, TARSKI:def 1;
take W =
W;
( W is open & P = product ({i} --> W) )thus
W is
open
by A3, A5;
P = product ({i} --> W)thus P =
product ((i .--> the carrier of (J . i)) +* (i,W))
by A2, A4, A5, FUNCOP_1:def 9
.=
product (i .--> W)
by Th44
.=
product ({i} --> W)
by FUNCOP_1:def 9
;
verum
end;
given V being Subset of (J . i) such that A6:
( V is open & P = product ({i} --> V) )
; P in product_prebasis J
P =
product (i .--> V)
by A6, FUNCOP_1:def 9
.=
product ((i .--> the carrier of (J . i)) +* (i,V))
by Th44
.=
product ((Carrier J) +* (i,V))
by A2, FUNCOP_1:def 9
;
hence
P in product_prebasis J
by A6, WAYBEL18:def 2; verum