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;

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

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

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

proof

assume A9:
i in rng f
; :: thesis: (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open
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;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

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