let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for P being non empty Subset of (product ()) st P in product_prebasis J holds
ex i being Element of I st
( (proj (J,i)) .: P is open & ( for j being Element of I st j <> i holds
(proj (J,j)) .: P = [#] (J . j) ) )

let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for P being non empty Subset of (product ()) st P in product_prebasis J holds
ex i being Element of I st
( (proj (J,i)) .: P is open & ( for j being Element of I st j <> i holds
(proj (J,j)) .: P = [#] (J . j) ) )

let P be non empty Subset of (product ()); :: thesis: ( P in product_prebasis J implies ex i being Element of I st
( (proj (J,i)) .: P is open & ( for j being Element of I st j <> i holds
(proj (J,j)) .: P = [#] (J . j) ) ) )

assume P in product_prebasis J ; :: thesis: ex i being Element of I st
( (proj (J,i)) .: P is open & ( for j being Element of I st j <> i holds
(proj (J,j)) .: P = [#] (J . j) ) )

then consider i being set , T being TopStruct , V being Subset of T such that
A1: ( i in I & V is open & T = J . i ) and
A2: P = product (() +* (i,V)) by WAYBEL18:def 2;
reconsider i = i as Element of I by A1;
reconsider V = V as Subset of (J . i) by A1;
take i ; :: thesis: ( (proj (J,i)) .: P is open & ( for j being Element of I st j <> i holds
(proj (J,j)) .: P = [#] (J . j) ) )

A3: dom () = I by PARTFUN1:def 2;
a4: rng (proj (J,i)) = the carrier of (J . i) by Th52;
(proj (J,i)) .: P = (proj (J,i)) .: ((proj (J,i)) " V) by ;
hence (proj (J,i)) .: P is open by ; :: thesis: for j being Element of I st j <> i holds
(proj (J,j)) .: P = [#] (J . j)

let j be Element of I; :: thesis: ( j <> i implies (proj (J,j)) .: P = [#] (J . j) )
assume A5: j <> i ; :: thesis: (proj (J,j)) .: P = [#] (J . j)
for x being object holds
( x in (proj (J,j)) .: P iff x in [#] (J . j) )
proof
let x be object ; :: thesis: ( x in (proj (J,j)) .: P iff x in [#] (J . j) )
hereby :: thesis: ( x in [#] (J . j) implies x in (proj (J,j)) .: P )
assume x in (proj (J,j)) .: P ; :: thesis: x in [#] (J . j)
then consider y being object such that
A6: ( y in dom (proj (J,j)) & y in P & x = (proj (J,j)) . y ) by FUNCT_1:def 6;
consider g being Function such that
A7: ( y = g & dom g = dom (() +* (i,V)) ) and
A8: for z being object st z in dom (() +* (i,V)) holds
g . z in (() +* (i,V)) . z by ;
j in dom () by A3;
then A9: j in dom (() +* (i,V)) by FUNCT_7:30;
x = g . j by ;
then x in (() +* (i,V)) . j by A8, A9;
then x in () . j by ;
hence x in [#] (J . j) by PENCIL_3:7; :: thesis: verum
end;
assume x in [#] (J . j) ; :: thesis: x in (proj (J,j)) .: P
then x in () . j by PENCIL_3:7;
then A10: x in (() +* (i,V)) . j by ;
set g0 = the Element of product (() +* (i,V));
set g = the Element of product (() +* (i,V)) +* (j,x);
a11: () . i = [#] (J . i) by PENCIL_3:7
.= the carrier of (J . i) by STRUCT_0:def 3 ;
consider g00 being Function such that
A12: ( the Element of product (() +* (i,V)) = g00 & dom g00 = dom (() +* (i,V)) ) and
A13: for z being object st z in dom (() +* (i,V)) holds
g00 . z in (() +* (i,V)) . z by ;
ex f being Function st
( the Element of product (() +* (i,V)) +* (j,x) = f & dom f = dom (() +* (i,V)) & ( for z being object st z in dom (() +* (i,V)) holds
f . z in (() +* (i,V)) . z ) )
proof
take the Element of product (() +* (i,V)) +* (j,x) ; :: thesis: ( the Element of product (() +* (i,V)) +* (j,x) = the Element of product (() +* (i,V)) +* (j,x) & dom ( the Element of product (() +* (i,V)) +* (j,x)) = dom (() +* (i,V)) & ( for z being object st z in dom (() +* (i,V)) holds
( the Element of product (() +* (i,V)) +* (j,x)) . z in (() +* (i,V)) . z ) )

thus ( the Element of product (() +* (i,V)) +* (j,x) = the Element of product (() +* (i,V)) +* (j,x) & dom ( the Element of product (() +* (i,V)) +* (j,x)) = dom (() +* (i,V)) ) by ; :: thesis: for z being object st z in dom (() +* (i,V)) holds
( the Element of product (() +* (i,V)) +* (j,x)) . z in (() +* (i,V)) . z

let z be object ; :: thesis: ( z in dom (() +* (i,V)) implies ( the Element of product (() +* (i,V)) +* (j,x)) . z in (() +* (i,V)) . z )
assume A15: z in dom (() +* (i,V)) ; :: thesis: ( the Element of product (() +* (i,V)) +* (j,x)) . z in (() +* (i,V)) . z
( z <> j implies ( the Element of product (() +* (i,V)) +* (j,x)) . z = the Element of product (() +* (i,V)) . z ) by FUNCT_7:32;
hence ( the Element of product (() +* (i,V)) +* (j,x)) . z in (() +* (i,V)) . z by ; :: thesis: verum
end;
then A16: the Element of product (() +* (i,V)) +* (j,x) in product (() +* (i,V)) by CARD_3:def 5;
a17: product (() +* (i,V)) c= product () by ;
then the Element of product (() +* (i,V)) +* (j,x) in product () by A16;
then the Element of product (() +* (i,V)) +* (j,x) in dom (proj ((),j)) by CARD_3:def 16;
then A18: the Element of product (() +* (i,V)) +* (j,x) in dom (proj (J,j)) by WAYBEL18:def 4;
A19: j in dom () by A3;
A20: the Element of product (() +* (i,V)) +* (j,x) is Element of () by ;
j in dom the Element of product (() +* (i,V)) by ;
then x = ( the Element of product (() +* (i,V)) +* (j,x)) . j by FUNCT_7:31
.= (proj (J,j)) . ( the Element of product (() +* (i,V)) +* (j,x)) by ;
hence x in (proj (J,j)) .: P by ; :: thesis: verum
end;
hence (proj (J,j)) .: P = [#] (J . j) by TARSKI:2; :: thesis: verum