let I be non empty set ; 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 (Carrier J)) st X c= product_prebasis J & dom f = X & f " is non-empty & ( for A being Subset of (product (Carrier J)) 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 ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) & ( i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open ) )
let J be non-Empty TopStruct-yielding ManySortedSet of I; for f being I -valued one-to-one Function
for X being Subset-Family of (product (Carrier J)) st X c= product_prebasis J & dom f = X & f " is non-empty & ( for A being Subset of (product (Carrier J)) 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 ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) & ( i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open ) )
let f be I -valued one-to-one Function; for X being Subset-Family of (product (Carrier J)) st X c= product_prebasis J & dom f = X & f " is non-empty & ( for A being Subset of (product (Carrier J)) 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 ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) & ( i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open ) )
let X be Subset-Family of (product (Carrier J)); ( X c= product_prebasis J & dom f = X & f " is non-empty & ( for A being Subset of (product (Carrier J)) 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 ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) & ( i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open ) ) )
set g = product_basis_selector (J,f);
set P = product ((Carrier J) +* (product_basis_selector (J,f)));
assume that
A1:
( X c= product_prebasis J & dom f = X & f " is non-empty )
and
A2:
for A being Subset of (product (Carrier J)) st A in X holds
(proj (J,(f /. A))) .: A is open
; for i being Element of I holds
( ( not i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) & ( i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open ) )
let i be Element of I; ( ( not i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) & ( i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open ) )
A3:
( dom (Carrier J) = I & dom (product_basis_selector (J,f)) = rng f )
by PARTFUN1:def 2;
A4:
product_basis_selector (J,f) is non-empty
by A1, Th55;
A6:
now for j being object st j in dom (product_basis_selector (J,f)) holds
(product_basis_selector (J,f)) . j c= (Carrier J) . jlet j be
object ;
( j in dom (product_basis_selector (J,f)) implies (product_basis_selector (J,f)) . j c= (Carrier J) . j )assume a7:
j in dom (product_basis_selector (J,f))
;
(product_basis_selector (J,f)) . j c= (Carrier J) . jthen
j in rng f
;
then reconsider k =
j as
Element of
I ;
(product_basis_selector (J,f)) . j = (proj (J,k)) .: ((f ") . k)
by a7, Th54;
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= (Carrier J) . j
by PENCIL_3:7;
verum end;
thus
( not i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) )
( i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open )proof
assume
not
i in rng f
;
(proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i)
then A8:
i in (dom (Carrier J)) \ (dom (product_basis_selector (J,f)))
by A3, XBOOLE_0:def 5;
thus (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) =
(proj ((Carrier J),i)) .: (product ((Carrier J) +* (product_basis_selector (J,f))))
by WAYBEL18:def 4
.=
(Carrier J) . i
by A3, A4, A6, A8, Th24
.=
[#] (J . i)
by PENCIL_3:7
;
verum
end;
assume A9:
i in rng f
; (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open
A11: (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) =
(proj ((Carrier J),i)) .: (product ((Carrier J) +* (product_basis_selector (J,f))))
by WAYBEL18:def 4
.=
(product_basis_selector (J,f)) . i
by A4, A3, A6, A9, Th25
.=
(proj (J,i)) .: ((f ") . i)
by A9, Th54
;
A12:
f . ((f ") . i) = i
by A9, FUNCT_1:35;
i in dom (f ")
by A9, FUNCT_1:33;
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 A1, a13, FUNCT_1:33;
then reconsider A = (f ") . i as Subset of (product (Carrier J)) ;
f /. A = i
by A12, A13, PARTFUN1:def 6;
hence
(proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open
by A2, A11, A13, A1; verum