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) )

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

hence
(proj (J,j)) .: P = [#] (J . j)
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in (proj (J,j)) .: P iff x in [#] (J . j) )

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 ) )

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;hereby :: thesis: ( x in [#] (J . j) implies x in (proj (J,j)) .: P )

assume
x in [#] (J . j)
; :: thesis: x in (proj (J,j)) .: Passume
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;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

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

then A16:
the Element of product ((Carrier J) +* (i,V)) +* (j,x) in product ((Carrier J) +* (i,V))
by CARD_3:def 5;
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;( 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

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