let I be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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)); :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( ( 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 :: thesis: for j being object st j in dom (product_basis_selector (J,f)) holds
(product_basis_selector (J,f)) . j c= (Carrier J) . j
let j be object ; :: thesis: ( 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)) ; :: thesis: (product_basis_selector (J,f)) . j c= (Carrier J) . j
then 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; :: thesis: verum
end;
thus ( not i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) :: thesis: ( 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 ; :: thesis: (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 ; :: thesis: verum
end;
assume A9: i in rng f ; :: thesis: (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; :: thesis: verum