for F being Function
for i, xi being set
for Ai being Subset of (F . i) st (proj F,i) " {xi} meets (proj F,i) " Ai holds
xi in Ai

for F, f being Function
for i, xi being set st xi in F . i & f in product F holds
f +* i,xi in product F

for F being Function
for i being set st i in dom F & product F <> {} holds
rng (proj F,i) = F . i

for F being Function
for i being set st i in dom F holds
(proj F,i) " (F . i) = product F

for F, f being Function
for i, xi being set st xi in F . i & i in dom F & f in product F holds
f +* i,xi in (proj F,i) " {xi}

for F, f being Function
for i1, i2, xi1 being set
for Ai2 being Subset of (F . i2) st xi1 in F . i1 & i1 in dom F & f in product F & i1 <> i2 holds
( f in (proj F,i2) " Ai2 iff f +* i1,xi1 in (proj F,i2) " Ai2 )

for F being Function
for i1, i2, xi1 being set
for Ai2 being Subset of (F . i2) st product F <> {} & xi1 in F . i1 & i1 in dom F & i2 in dom F & Ai2 <> F . i2 holds
( (proj F,i1) " {xi1} c= (proj F,i2) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for f being Element of (product J) holds (proj J,i) . f = f . i

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for Ai being Subset of (J . i) st (proj J,i) " {xi} meets (proj J,i) " Ai holds
xi in Ai

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I holds (proj J,i) " ([#] (J . i)) = [#] (product J)

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for f being Element of (product J) holds f +* i,xi in (proj J,i) " {xi}

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i1, i2 being Element of I
for xi1 being Element of (J . i1)
for Ai2 being Subset of (J . i2) st Ai2 <> [#] (J . i2) holds
( (proj J,i1) " {xi1} c= (proj J,i2) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i1, i2 being Element of I
for xi1 being Element of (J . i1)
for Ai2 being Subset of (J . i2)
for f being Element of (product J) st i1 <> i2 holds
( f in (proj J,i2) " Ai2 iff f +* i1,xi1 in (proj J,i2) " Ai2 )

for T being non empty TopStruct holds
( T is compact iff for F being Subset-Family of T st F is open & [#] T c= union F holds
ex G being Subset-Family of T st
( G c= F & [#] T c= union G & G is finite ) )

for T being non empty TopSpace
for B being prebasis of T holds
( T is compact iff for F being Subset of B st [#] T c= union F holds
ex G being finite Subset of F st [#] T c= union G )

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for A being set st A in product_prebasis J holds
ex i being Element of I ex Ai being Subset of (J . i) st
( Ai is open & (proj J,i) " Ai = A )

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for A being set st A in product_prebasis J & (proj J,i) " {xi} c= A & not A = [#] (product J) holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj J,i) " Ai )

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for Fi being non empty Subset-Family of (J . i) st [#] (J . i) c= union Fi holds
[#] (product J) c= union { ((proj J,i) " Ai) where Ai is Element of Fi : verum }

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for G being Subset of (product_prebasis J) st (proj J,i) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj J,i) " {xi} c= A ) holds
[#] (product J) c= union G

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj J,i) " {xi} c= union G holds
ex A being set st
( A in product_prebasis J & A in G & (proj J,i) " {xi} c= A )

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj J,i) " {xi} c= union G holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj J,i) " Ai in G & Ai is open )

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for F being Subset of (product_prebasis J) st ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
ex xi being Element of (J . i) st
for G being finite Subset of F holds not (proj J,i) " {xi} c= union G

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I st ( for i being Element of I holds J . i is compact ) holds
product J is compact