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)

proof

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;

rng f = <:(proj (J,i)),(proj (J,j)):> .: (dom f) by A1, RELAT_1:113
.= <:(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

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 )

proof

per cases ( P <> {} or P = {} ) ;

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;

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;

end;

end;

A7: ex F being ManySortedSet of I st
( P = product F & ( for k being Element of I holds F . k c= (Carrier J) . k ) )

proof

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

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

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;

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;

end;

end;

P is Subset of (product (Carrier J)) by WAYBEL18:def 3;
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;

hence f is open by Th45; :: thesis: verum