let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I

for i, j being Element of I

for f being Function of (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds

( f is onto & f is open )

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i, j being Element of I

for f being Function of (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds

( f is onto & f is open )

let i, j be Element of I; :: thesis: for f being Function of (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds

( f is onto & f is open )

let f be Function of (product J),[:(J . i),(J . j):]; :: thesis: ( i <> j & f = <:(proj (J,i)),(proj (J,j)):> implies ( f is onto & f is open ) )

assume A1: ( i <> j & f = <:(proj (J,i)),(proj (J,j)):> ) ; :: thesis: ( f is onto & f is open )

a2: for k being Element of I holds (Carrier J) . k c= (Carrier J) . k ;

A3: for k being Element of I holds (proj (J,k)) .: ([#] (product (Carrier J))) = the carrier of (J . k)

.= <:(proj (J,i)),(proj (J,j)):> .: the carrier of (product J) by FUNCT_2:def 1

.= <:(proj (J,i)),(proj (J,j)):> .: (product (Carrier J)) by WAYBEL18:def 3

.= <:(proj (J,i)),(proj (J,j)):> .: ([#] (product (Carrier J))) by SUBSET_1:def 3

.= [:((proj (J,i)) .: ([#] (product (Carrier J)))),((proj (J,j)) .: ([#] (product (Carrier J)))):] by A1, SUBSET_1:def 3, a2, Th72

.= [: the carrier of (J . i),((proj (J,j)) .: ([#] (product (Carrier J)))):] by A3

.= [: the carrier of (J . i), the carrier of (J . j):] by A3

.= the carrier of [:(J . i),(J . j):] by BORSUK_1:def 2 ;

hence f is onto by FUNCT_2:def 3; :: thesis: f is open

ex B being Basis of (product J) st

for P being Subset of (product J) st P in B holds

f .: P is open

for i, j being Element of I

for f being Function of (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds

( f is onto & f is open )

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i, j being Element of I

for f being Function of (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds

( f is onto & f is open )

let i, j be Element of I; :: thesis: for f being Function of (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds

( f is onto & f is open )

let f be Function of (product J),[:(J . i),(J . j):]; :: thesis: ( i <> j & f = <:(proj (J,i)),(proj (J,j)):> implies ( f is onto & f is open ) )

assume A1: ( i <> j & f = <:(proj (J,i)),(proj (J,j)):> ) ; :: thesis: ( f is onto & f is open )

a2: for k being Element of I holds (Carrier J) . k c= (Carrier J) . k ;

A3: for k being Element of I holds (proj (J,k)) .: ([#] (product (Carrier J))) = the carrier of (J . k)

proof

rng f =
<:(proj (J,i)),(proj (J,j)):> .: (dom f)
by A1, RELAT_1:113
let k be Element of I; :: thesis: (proj (J,k)) .: ([#] (product (Carrier J))) = the carrier of (J . k)

thus (proj (J,k)) .: ([#] (product (Carrier J))) = (proj (J,k)) .: (product (Carrier J)) by SUBSET_1:def 3

.= (proj (J,k)) .: (dom (proj ((Carrier J),k))) by CARD_3:def 16

.= (proj (J,k)) .: (dom (proj (J,k))) by WAYBEL18:def 4

.= rng (proj (J,k)) by RELAT_1:113

.= the carrier of (J . k) by Th52 ; :: thesis: verum

end;thus (proj (J,k)) .: ([#] (product (Carrier J))) = (proj (J,k)) .: (product (Carrier J)) by SUBSET_1:def 3

.= (proj (J,k)) .: (dom (proj ((Carrier J),k))) by CARD_3:def 16

.= (proj (J,k)) .: (dom (proj (J,k))) by WAYBEL18:def 4

.= rng (proj (J,k)) by RELAT_1:113

.= the carrier of (J . k) by Th52 ; :: thesis: verum

.= <:(proj (J,i)),(proj (J,j)):> .: the carrier of (product J) by FUNCT_2:def 1

.= <:(proj (J,i)),(proj (J,j)):> .: (product (Carrier J)) by WAYBEL18:def 3

.= <:(proj (J,i)),(proj (J,j)):> .: ([#] (product (Carrier J))) by SUBSET_1:def 3

.= [:((proj (J,i)) .: ([#] (product (Carrier J)))),((proj (J,j)) .: ([#] (product (Carrier J)))):] by A1, SUBSET_1:def 3, a2, Th72

.= [: the carrier of (J . i),((proj (J,j)) .: ([#] (product (Carrier J)))):] by A3

.= [: the carrier of (J . i), the carrier of (J . j):] by A3

.= the carrier of [:(J . i),(J . j):] by BORSUK_1:def 2 ;

hence f is onto by FUNCT_2:def 3; :: thesis: f is open

ex B being Basis of (product J) st

for P being Subset of (product J) st P in B holds

f .: P is open

proof

hence
f is open
by Th45; :: thesis: verum
set B = FinMeetCl (product_prebasis J);

set T = product J;

reconsider K = product_prebasis J as Subset-Family of (product J) by WAYBEL18:def 3;

FinMeetCl K is Basis of (product J) by WAYBEL18:def 3, YELLOW_9:23;

then reconsider B = FinMeetCl (product_prebasis J) as Basis of (product J) by WAYBEL18:def 3;

take B ; :: thesis: for P being Subset of (product J) st P in B holds

f .: P is open

let P be Subset of (product J); :: thesis: ( P in B implies f .: P is open )

assume A4: P in B ; :: thesis: f .: P is open

A5: ( (proj (J,i)) .: P is open & (proj (J,j)) .: P is open )

( P = product F & ( for k being Element of I holds F . k c= (Carrier J) . k ) )

then f .: P = [:((proj (J,i)) .: P),((proj (J,j)) .: P):] by A1, A7, Th72;

hence f .: P is open by A5, BORSUK_1:6; :: thesis: verum

end;set T = product J;

reconsider K = product_prebasis J as Subset-Family of (product J) by WAYBEL18:def 3;

FinMeetCl K is Basis of (product J) by WAYBEL18:def 3, YELLOW_9:23;

then reconsider B = FinMeetCl (product_prebasis J) as Basis of (product J) by WAYBEL18:def 3;

take B ; :: thesis: for P being Subset of (product J) st P in B holds

f .: P is open

let P be Subset of (product J); :: thesis: ( P in B implies f .: P is open )

assume A4: P in B ; :: thesis: f .: P is open

A5: ( (proj (J,i)) .: P is open & (proj (J,j)) .: P is open )

proof
end;

A7:
ex F being ManySortedSet of I st per cases
( P <> {} or P = {} )
;

end;

suppose
P <> {}
; :: thesis: ( (proj (J,i)) .: P is open & (proj (J,j)) .: P is open )

then
ex I0 being finite Subset of I st

for j being Element of I holds

( (proj (J,j)) .: P is open & ( not j in I0 implies (proj (J,j)) .: P = [#] (J . j) ) ) by A4, Th63;

hence ( (proj (J,i)) .: P is open & (proj (J,j)) .: P is open ) ; :: thesis: verum

end;for j being Element of I holds

( (proj (J,j)) .: P is open & ( not j in I0 implies (proj (J,j)) .: P = [#] (J . j) ) ) by A4, Th63;

hence ( (proj (J,i)) .: P is open & (proj (J,j)) .: P is open ) ; :: thesis: verum

suppose
P = {}
; :: thesis: ( (proj (J,i)) .: P is open & (proj (J,j)) .: P is open )

then
( (proj (J,i)) .: P is empty & (proj (J,i)) .: P is Subset of (J . i) & (proj (J,j)) .: P is empty & (proj (J,j)) .: P is Subset of (J . j) )
;

hence ( (proj (J,i)) .: P is open & (proj (J,j)) .: P is open ) ; :: thesis: verum

end;hence ( (proj (J,i)) .: P is open & (proj (J,j)) .: P is open ) ; :: thesis: verum

( P = product F & ( for k being Element of I holds F . k c= (Carrier J) . k ) )

proof

P is Subset of (product (Carrier J))
by WAYBEL18:def 3;
consider X being Subset-Family of (product (Carrier J)), g being I -valued one-to-one Function such that

( X c= product_prebasis J & X is finite & P = Intersect X & dom g = X ) and

A8: P = product ((Carrier J) +* (product_basis_selector (J,g))) by A4, Lm3;

set F = (Carrier J) +* (product_basis_selector (J,g));

reconsider F = (Carrier J) +* (product_basis_selector (J,g)) as ManySortedSet of I ;

take F ; :: thesis: ( P = product F & ( for k being Element of I holds F . k c= (Carrier J) . k ) )

thus P = product F by A8; :: thesis: for k being Element of I holds F . k c= (Carrier J) . k

let k be Element of I; :: thesis: F . k c= (Carrier J) . k

end;( X c= product_prebasis J & X is finite & P = Intersect X & dom g = X ) and

A8: P = product ((Carrier J) +* (product_basis_selector (J,g))) by A4, Lm3;

set F = (Carrier J) +* (product_basis_selector (J,g));

reconsider F = (Carrier J) +* (product_basis_selector (J,g)) as ManySortedSet of I ;

take F ; :: thesis: ( P = product F & ( for k being Element of I holds F . k c= (Carrier J) . k ) )

thus P = product F by A8; :: thesis: for k being Element of I holds F . k c= (Carrier J) . k

let k be Element of I; :: thesis: F . k c= (Carrier J) . k

per cases
( k in rng g or not k in rng g )
;

end;

suppose A9:
k in rng g
; :: thesis: F . k c= (Carrier J) . k

then
k in dom (product_basis_selector (J,g))
by PARTFUN1:def 2;

then a10: F . k = (product_basis_selector (J,g)) . k by FUNCT_4:13

.= (proj (J,k)) .: ((g ") . k) by A9, Th54 ;

rng (proj (J,k)) = the carrier of (J . k) by Th52

.= [#] (J . k) by STRUCT_0:def 3

.= (Carrier J) . k by PENCIL_3:7 ;

hence F . k c= (Carrier J) . k by a10, RELAT_1:111; :: thesis: verum

end;then a10: F . k = (product_basis_selector (J,g)) . k by FUNCT_4:13

.= (proj (J,k)) .: ((g ") . k) by A9, Th54 ;

rng (proj (J,k)) = the carrier of (J . k) by Th52

.= [#] (J . k) by STRUCT_0:def 3

.= (Carrier J) . k by PENCIL_3:7 ;

hence F . k c= (Carrier J) . k by a10, RELAT_1:111; :: thesis: verum

suppose
not k in rng g
; :: thesis: F . k c= (Carrier J) . k

then
not k in dom (product_basis_selector (J,g))
;

hence F . k c= (Carrier J) . k by FUNCT_4:11; :: thesis: verum

end;hence F . k c= (Carrier J) . k by FUNCT_4:11; :: thesis: verum

then f .: P = [:((proj (J,i)) .: P),((proj (J,j)) .: P):] by A1, A7, Th72;

hence f .: P is open by A5, BORSUK_1:6; :: thesis: verum