let I be non empty set ; 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; 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)); ( 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
; 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
; ( (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; for j being Element of I st j <> i holds
(proj (J,j)) .: P = [#] (J . j)
let j be Element of I; ( j <> i implies (proj (J,j)) .: P = [#] (J . j) )
assume A5:
j <> i
; (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 ;
( x in (proj (J,j)) .: P iff x in [#] (J . j) )
hereby ( x in [#] (J . j) implies x in (proj (J,j)) .: P )
assume
x in (proj (J,j)) .: P
;
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;
verum
end;
assume
x in [#] (J . j)
;
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)
;
( 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;
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 ;
( 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))
;
( 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;
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;
verum
end;
hence
(proj (J,j)) .: P = [#] (J . j)
by TARSKI:2; verum