let I be non empty set ; :: thesis: for J being non-Empty TopStruct-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
( ( not i in rng f implies (proj (J,i)) .: (product (() +* ())) = [#] (J . i) ) & ( i in rng f implies (proj (J,i)) .: (product (() +* ())) is open ) )

let J be non-Empty TopStruct-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
( ( not i in rng f implies (proj (J,i)) .: (product (() +* ())) = [#] (J . i) ) & ( i in rng f implies (proj (J,i)) .: (product (() +* ())) is open ) )

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
( ( not i in rng f implies (proj (J,i)) .: (product (() +* ())) = [#] (J . i) ) & ( i in rng f implies (proj (J,i)) .: (product (() +* ())) is open ) )

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
( ( not i in rng f implies (proj (J,i)) .: (product (() +* ())) = [#] (J . i) ) & ( i in rng f implies (proj (J,i)) .: (product (() +* ())) is open ) ) )

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
( ( not i in rng f implies (proj (J,i)) .: (product (() +* ())) = [#] (J . i) ) & ( i in rng f implies (proj (J,i)) .: (product (() +* ())) is open ) )

let i be Element of I; :: thesis: ( ( not i in rng f implies (proj (J,i)) .: (product (() +* ())) = [#] (J . i) ) & ( i in rng f implies (proj (J,i)) .: (product (() +* ())) is open ) )
A3: ( dom () = I & dom () = rng f ) by PARTFUN1:def 2;
A4: product_basis_selector (J,f) is non-empty by ;
A6: now :: thesis: for j being object st j in dom () holds
() . j c= () . j
let j be object ; :: thesis: ( j in dom () implies () . j c= () . j )
assume a7: j in dom () ; :: thesis: () . j c= () . j
then j in rng f ;
then reconsider k = j as Element of I ;
(product_basis_selector (J,f)) . j = (proj (J,k)) .: ((f ") . k) by ;
then (product_basis_selector (J,f)) . j c= the carrier of (J . k) ;
then (product_basis_selector (J,f)) . j c= [#] (J . k) by STRUCT_0:def 3;
hence (product_basis_selector (J,f)) . j c= () . j by PENCIL_3:7; :: thesis: verum
end;
thus ( not i in rng f implies (proj (J,i)) .: (product (() +* ())) = [#] (J . i) ) :: thesis: ( i in rng f implies (proj (J,i)) .: (product (() +* ())) is open )
proof
assume not i in rng f ; :: thesis: (proj (J,i)) .: (product (() +* ())) = [#] (J . i)
then A8: i in (dom ()) \ (dom ()) by ;
thus (proj (J,i)) .: (product (() +* ())) = (proj ((),i)) .: (product (() +* ())) by WAYBEL18:def 4
.= () . i by A3, A4, A6, A8, Th24
.= [#] (J . i) by PENCIL_3:7 ; :: thesis: verum
end;
assume A9: i in rng f ; :: thesis: (proj (J,i)) .: (product (() +* ())) is open
A11: (proj (J,i)) .: (product (() +* ())) = (proj ((),i)) .: (product (() +* ())) by WAYBEL18:def 4
.= () . i by A4, A3, A6, A9, Th25
.= (proj (J,i)) .: ((f ") . i) by ;
A12: f . ((f ") . i) = i by ;
i in dom (f ") by ;
then a13: (f ") . i in rng (f ") by FUNCT_1:3;
then A13: (f ") . i in dom f by FUNCT_1:33;
(f ") . i in X by ;
then reconsider A = (f ") . i as Subset of (product ()) ;
f /. A = i by ;
hence (proj (J,i)) .: (product (() +* ())) is open by A2, A11, A13, A1; :: thesis: verum