let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for f being I -valued one-to-one Function
for X being Subset-Family of (product (Carrier J)) st X c= product_prebasis J & dom f = X & f " is non-empty & ( for A being Subset of (product (Carrier J)) st A in X holds
(proj (J,(f /. A))) .: A is open ) holds
for i being Element of I holds
( (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open & ( not i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) )
let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for f being I -valued one-to-one Function
for X being Subset-Family of (product (Carrier J)) st X c= product_prebasis J & dom f = X & f " is non-empty & ( for A being Subset of (product (Carrier J)) st A in X holds
(proj (J,(f /. A))) .: A is open ) holds
for i being Element of I holds
( (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open & ( not i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) )
let f be I -valued one-to-one Function; :: thesis: for X being Subset-Family of (product (Carrier J)) st X c= product_prebasis J & dom f = X & f " is non-empty & ( for A being Subset of (product (Carrier J)) st A in X holds
(proj (J,(f /. A))) .: A is open ) holds
for i being Element of I holds
( (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open & ( not i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) )
let X be Subset-Family of (product (Carrier J)); :: thesis: ( X c= product_prebasis J & dom f = X & f " is non-empty & ( for A being Subset of (product (Carrier J)) st A in X holds
(proj (J,(f /. A))) .: A is open ) implies for i being Element of I holds
( (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open & ( not i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) ) )
set g = product_basis_selector (J,f);
set P = product ((Carrier J) +* (product_basis_selector (J,f)));
assume that
A1: ( X c= product_prebasis J & dom f = X & f " is non-empty ) and
A2: for A being Subset of (product (Carrier J)) st A in X holds
(proj (J,(f /. A))) .: A is open ; :: thesis: for i being Element of I holds
( (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open & ( not i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) )
let i be Element of I; :: thesis: ( (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open & ( not i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) )
( not i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) by A1, A2, Th59;
hence ( (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open & ( not i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) ) by A1, A2, Th59; :: thesis: verum