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 (),[:(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 (),[:(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 (),[:(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 (),[:(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 () . k c= () . k ;
A3: for k being Element of I holds (proj (J,k)) .: ([#] (product ())) = the carrier of (J . k)
proof
let k be Element of I; :: thesis: (proj (J,k)) .: ([#] (product ())) = the carrier of (J . k)
thus (proj (J,k)) .: ([#] (product ())) = (proj (J,k)) .: (product ()) by SUBSET_1:def 3
.= (proj (J,k)) .: (dom (proj ((),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
.= <:(proj (J,i)),(proj (J,j)):> .: the carrier of () by FUNCT_2:def 1
.= <:(proj (J,i)),(proj (J,j)):> .: (product ()) by WAYBEL18:def 3
.= <:(proj (J,i)),(proj (J,j)):> .: ([#] (product ())) by SUBSET_1:def 3
.= [:((proj (J,i)) .: ([#] (product ()))),((proj (J,j)) .: ([#] (product ()))):] by
.= [: the carrier of (J . i),((proj (J,j)) .: ([#] (product ()))):] 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 () st
for P being Subset of () st P in B holds
f .: P is open
proof
set B = FinMeetCl ();
set T = product J;
reconsider K = product_prebasis J as Subset-Family of () by WAYBEL18:def 3;
FinMeetCl K is Basis of () by ;
then reconsider B = FinMeetCl () as Basis of () by WAYBEL18:def 3;
take B ; :: thesis: for P being Subset of () st P in B holds
f .: P is open

let P be Subset of (); :: 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 ;
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= () . k ) )
proof
consider X being Subset-Family of (product ()), 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 (() +* ()) by ;
set F = () +* ();
reconsider F = () +* () as ManySortedSet of I ;
take F ; :: thesis: ( P = product F & ( for k being Element of I holds F . k c= () . k ) )
thus P = product F by A8; :: thesis: for k being Element of I holds F . k c= () . k
let k be Element of I; :: thesis: F . k c= () . k
per cases ( k in rng g or not k in rng g ) ;
suppose A9: k in rng g ; :: thesis: F . k c= () . k
then k in dom () by PARTFUN1:def 2;
then a10: F . k = () . k by FUNCT_4:13
.= (proj (J,k)) .: ((g ") . k) by ;
rng (proj (J,k)) = the carrier of (J . k) by Th52
.= [#] (J . k) by STRUCT_0:def 3
.= () . k by PENCIL_3:7 ;
hence F . k c= () . k by ; :: thesis: verum
end;
end;
end;
P is Subset of (product ()) 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 ; :: thesis: verum
end;
hence f is open by Th45; :: thesis: verum