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

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