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 (Carrier J)) 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 (Carrier J)) 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 (Carrier J)); :: 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 ((Carrier J) +* (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 (Carrier J) = 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 A2, WAYBEL18:4;
hence (proj (J,i)) .: P is open by A1, a4, FUNCT_1:77; :: 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 ((Carrier J) +* (i,V)) ) and
A8: for z being object st z in dom ((Carrier J) +* (i,V)) holds
g . z in ((Carrier J) +* (i,V)) . z by A2, A6, CARD_3:def 5;
j in dom (Carrier J) by A3;
then A9: j in dom ((Carrier J) +* (i,V)) by FUNCT_7:30;
x = g . j by A6, A7, YELLOW17:8;
then x in ((Carrier J) +* (i,V)) . j by A8, A9;
then x in (Carrier J) . j by A5, FUNCT_7:32;
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 (Carrier J) . j by PENCIL_3:7;
then A10: x in ((Carrier J) +* (i,V)) . j by A5, FUNCT_7:32;
set g0 = the Element of product ((Carrier J) +* (i,V));
set g = the Element of product ((Carrier J) +* (i,V)) +* (j,x);
a11: (Carrier J) . 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 ((Carrier J) +* (i,V)) = g00 & dom g00 = dom ((Carrier J) +* (i,V)) ) and
A13: for z being object st z in dom ((Carrier J) +* (i,V)) holds
g00 . z in ((Carrier J) +* (i,V)) . z by A2, CARD_3:def 5;
ex f being Function st
( the Element of product ((Carrier J) +* (i,V)) +* (j,x) = f & dom f = dom ((Carrier J) +* (i,V)) & ( for z being object st z in dom ((Carrier J) +* (i,V)) holds
f . z in ((Carrier J) +* (i,V)) . z ) )

proof

take the Element of product ((Carrier J) +* (i,V)) +* (j,x) ; :: thesis: ( the Element of product ((Carrier J) +* (i,V)) +* (j,x) = the Element of product ((Carrier J) +* (i,V)) +* (j,x) & dom ( the Element of product ((Carrier J) +* (i,V)) +* (j,x)) = dom ((Carrier J) +* (i,V)) & ( for z being object st z in dom ((Carrier J) +* (i,V)) holds
( the Element of product ((Carrier J) +* (i,V)) +* (j,x)) . z in ((Carrier J) +* (i,V)) . z ) )
thus ( the Element of product ((Carrier J) +* (i,V)) +* (j,x) = the Element of product ((Carrier J) +* (i,V)) +* (j,x) & dom ( the Element of product ((Carrier J) +* (i,V)) +* (j,x)) = dom ((Carrier J) +* (i,V)) ) by A12, FUNCT_7:30; :: thesis: for z being object st z in dom ((Carrier J) +* (i,V)) holds
( the Element of product ((Carrier J) +* (i,V)) +* (j,x)) . z in ((Carrier J) +* (i,V)) . z
let z be object ; :: thesis: ( z in dom ((Carrier J) +* (i,V)) implies ( the Element of product ((Carrier J) +* (i,V)) +* (j,x)) . z in ((Carrier J) +* (i,V)) . z )
assume A15: z in dom ((Carrier J) +* (i,V)) ; :: thesis: ( the Element of product ((Carrier J) +* (i,V)) +* (j,x)) . z in ((Carrier J) +* (i,V)) . z
( z <> j implies ( the Element of product ((Carrier J) +* (i,V)) +* (j,x)) . z = the Element of product ((Carrier J) +* (i,V)) . z ) by FUNCT_7:32;
hence ( the Element of product ((Carrier J) +* (i,V)) +* (j,x)) . z in ((Carrier J) +* (i,V)) . z by A10, A12, A13, A15, FUNCT_7:31; :: thesis: verum

end;

then A16: the Element of product ((Carrier J) +* (i,V)) +* (j,x) in product ((Carrier J) +* (i,V)) by CARD_3:def 5;
a17: product ((Carrier J) +* (i,V)) c= product (Carrier J) by A3, a11, Th39;
then the Element of product ((Carrier J) +* (i,V)) +* (j,x) in product (Carrier J) by A16;
then the Element of product ((Carrier J) +* (i,V)) +* (j,x) in dom (proj ((Carrier J),j)) by CARD_3:def 16;
then A18: the Element of product ((Carrier J) +* (i,V)) +* (j,x) in dom (proj (J,j)) by WAYBEL18:def 4;
A19: j in dom (Carrier J) by A3;
A20: the Element of product ((Carrier J) +* (i,V)) +* (j,x) is Element of (product J) by a17, A16, WAYBEL18:def 3;
j in dom the Element of product ((Carrier J) +* (i,V)) by A12, A19, FUNCT_7:30;
then x = ( the Element of product ((Carrier J) +* (i,V)) +* (j,x)) . j by FUNCT_7:31
.= (proj (J,j)) . ( the Element of product ((Carrier J) +* (i,V)) +* (j,x)) by A20, YELLOW17:8 ;
hence x in (proj (J,j)) .: P by A2, A16, A18, FUNCT_1:def 6; :: thesis: verum

end;

hence (proj (J,j)) .: P = [#] (J . j) by TARSKI:2; :: thesis: verum