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 ()) st X c= product_prebasis J & dom f = X & f " is non-empty & ( for A being Subset of (product ()) st A in X holds
(proj (J,(f /. A))) .: A is open ) holds
for i being Element of I holds
( (proj (J,i)) .: (product (() +* ())) is open & ( not i in rng f implies (proj (J,i)) .: (product (() +* ())) = [#] (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 ()) st X c= product_prebasis J & dom f = X & f " is non-empty & ( for A being Subset of (product ()) st A in X holds
(proj (J,(f /. A))) .: A is open ) holds
for i being Element of I holds
( (proj (J,i)) .: (product (() +* ())) is open & ( not i in rng f implies (proj (J,i)) .: (product (() +* ())) = [#] (J . i) ) )

let f be I -valued one-to-one Function; :: thesis: for X being Subset-Family of (product ()) st X c= product_prebasis J & dom f = X & f " is non-empty & ( for A being Subset of (product ()) st A in X holds
(proj (J,(f /. A))) .: A is open ) holds
for i being Element of I holds
( (proj (J,i)) .: (product (() +* ())) is open & ( not i in rng f implies (proj (J,i)) .: (product (() +* ())) = [#] (J . i) ) )

let X be Subset-Family of (product ()); :: thesis: ( X c= product_prebasis J & dom f = X & f " is non-empty & ( for A being Subset of (product ()) st A in X holds
(proj (J,(f /. A))) .: A is open ) implies for i being Element of I holds
( (proj (J,i)) .: (product (() +* ())) is open & ( not i in rng f implies (proj (J,i)) .: (product (() +* ())) = [#] (J . i) ) ) )

set g = product_basis_selector (J,f);
set P = product (() +* ());
assume that
A1: ( X c= product_prebasis J & dom f = X & f " is non-empty ) and
A2: for A being Subset of (product ()) st A in X holds
(proj (J,(f /. A))) .: A is open ; :: thesis: for i being Element of I holds
( (proj (J,i)) .: (product (() +* ())) is open & ( not i in rng f implies (proj (J,i)) .: (product (() +* ())) = [#] (J . i) ) )

let i be Element of I; :: thesis: ( (proj (J,i)) .: (product (() +* ())) is open & ( not i in rng f implies (proj (J,i)) .: (product (() +* ())) = [#] (J . i) ) )
( not i in rng f implies (proj (J,i)) .: (product (() +* ())) = [#] (J . i) ) by A1, A2, Th59;
hence ( (proj (J,i)) .: (product (() +* ())) is open & ( not i in rng f implies (proj (J,i)) .: (product (() +* ())) = [#] (J . i) ) ) by A1, A2, Th59; :: thesis: verum