let i, j be Element of NAT ; :: thesis: ex f being Function of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):],(TopSpaceMetr (Euclid (i + j))) st

( f is being_homeomorphism & ( for fi, fj being FinSequence st [fi,fj] in dom f holds

f . (fi,fj) = fi ^ fj ) )

set ci = the carrier of (Euclid i);

set cj = the carrier of (Euclid j);

set cij = the carrier of (Euclid (i + j));

defpred S_{1}[ Element of the carrier of (Euclid i), Element of the carrier of (Euclid j), set ] means ex fi, fj being FinSequence of REAL st

( fi = $1 & fj = $2 & $3 = fi ^ fj );

A1: the carrier of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) = the carrier of (max-Prod2 ((Euclid i),(Euclid j))) by TOPMETR:12;

A2: for x being Element of the carrier of (Euclid i)

for y being Element of the carrier of (Euclid j) ex u being Element of the carrier of (Euclid (i + j)) st S_{1}[x,y,u]

A3: for x being Element of the carrier of (Euclid i)

for y being Element of the carrier of (Euclid j) holds S_{1}[x,y,f . (x,y)]
from BINOP_1:sch 3(A2);

A4: [: the carrier of (Euclid i), the carrier of (Euclid j):] = the carrier of (max-Prod2 ((Euclid i),(Euclid j))) by Def1;

the carrier of (TopSpaceMetr (Euclid (i + j))) = the carrier of (Euclid (i + j)) by TOPMETR:12;

then reconsider f = f as Function of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))),(TopSpaceMetr (Euclid (i + j))) by A4, A1;

A5: [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] = TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j))) by Th23;

then reconsider f = f as Function of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):],(TopSpaceMetr (Euclid (i + j))) ;

take f ; :: thesis: ( f is being_homeomorphism & ( for fi, fj being FinSequence st [fi,fj] in dom f holds

f . (fi,fj) = fi ^ fj ) )

thus dom f = [#] [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] by FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( rng f = [#] (TopSpaceMetr (Euclid (i + j))) & f is one-to-one & f is continuous & f " is continuous & ( for fi, fj being FinSequence st [fi,fj] in dom f holds

f . (fi,fj) = fi ^ fj ) )

thus A6: rng f = [#] (TopSpaceMetr (Euclid (i + j))) :: thesis: ( f is one-to-one & f is continuous & f " is continuous & ( for fi, fj being FinSequence st [fi,fj] in dom f holds

f . (fi,fj) = fi ^ fj ) )

f . (fi,fj) = fi ^ fj ) )

(f ") " P is open

f " P is open

hence f is continuous by A56, TOPS_2:43; :: thesis: ( f " is continuous & ( for fi, fj being FinSequence st [fi,fj] in dom f holds

f . (fi,fj) = fi ^ fj ) )

[#] (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) <> {} ;

hence f " is continuous by A27, A5, TOPS_2:43; :: thesis: for fi, fj being FinSequence st [fi,fj] in dom f holds

f . (fi,fj) = fi ^ fj

let fi, fj be FinSequence; :: thesis: ( [fi,fj] in dom f implies f . (fi,fj) = fi ^ fj )

assume A76: [fi,fj] in dom f ; :: thesis: f . (fi,fj) = fi ^ fj

then reconsider Fi = fi as Element of the carrier of (Euclid i) by A1, A5, A4, ZFMISC_1:87;

reconsider Fj = fj as Element of the carrier of (Euclid j) by A76, A1, A5, A4, ZFMISC_1:87;

S_{1}[Fi,Fj,f . (Fi,Fj)]
by A3;

hence f . (fi,fj) = fi ^ fj ; :: thesis: verum

( f is being_homeomorphism & ( for fi, fj being FinSequence st [fi,fj] in dom f holds

f . (fi,fj) = fi ^ fj ) )

set ci = the carrier of (Euclid i);

set cj = the carrier of (Euclid j);

set cij = the carrier of (Euclid (i + j));

defpred S

( fi = $1 & fj = $2 & $3 = fi ^ fj );

A1: the carrier of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) = the carrier of (max-Prod2 ((Euclid i),(Euclid j))) by TOPMETR:12;

A2: for x being Element of the carrier of (Euclid i)

for y being Element of the carrier of (Euclid j) ex u being Element of the carrier of (Euclid (i + j)) st S

proof

consider f being Function of [: the carrier of (Euclid i), the carrier of (Euclid j):], the carrier of (Euclid (i + j)) such that
let x be Element of the carrier of (Euclid i); :: thesis: for y being Element of the carrier of (Euclid j) ex u being Element of the carrier of (Euclid (i + j)) st S_{1}[x,y,u]

let y be Element of the carrier of (Euclid j); :: thesis: ex u being Element of the carrier of (Euclid (i + j)) st S_{1}[x,y,u]

( x is Element of REAL i & y is Element of REAL j ) ;

then reconsider fi = x, fj = y as FinSequence of REAL ;

fi ^ fj is Tuple of i + j, REAL by FINSEQ_2:107;

then reconsider u = fi ^ fj as Element of the carrier of (Euclid (i + j)) by FINSEQ_2:131;

take u ; :: thesis: S_{1}[x,y,u]

thus S_{1}[x,y,u]
; :: thesis: verum

end;let y be Element of the carrier of (Euclid j); :: thesis: ex u being Element of the carrier of (Euclid (i + j)) st S

( x is Element of REAL i & y is Element of REAL j ) ;

then reconsider fi = x, fj = y as FinSequence of REAL ;

fi ^ fj is Tuple of i + j, REAL by FINSEQ_2:107;

then reconsider u = fi ^ fj as Element of the carrier of (Euclid (i + j)) by FINSEQ_2:131;

take u ; :: thesis: S

thus S

A3: for x being Element of the carrier of (Euclid i)

for y being Element of the carrier of (Euclid j) holds S

A4: [: the carrier of (Euclid i), the carrier of (Euclid j):] = the carrier of (max-Prod2 ((Euclid i),(Euclid j))) by Def1;

the carrier of (TopSpaceMetr (Euclid (i + j))) = the carrier of (Euclid (i + j)) by TOPMETR:12;

then reconsider f = f as Function of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))),(TopSpaceMetr (Euclid (i + j))) by A4, A1;

A5: [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] = TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j))) by Th23;

then reconsider f = f as Function of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):],(TopSpaceMetr (Euclid (i + j))) ;

take f ; :: thesis: ( f is being_homeomorphism & ( for fi, fj being FinSequence st [fi,fj] in dom f holds

f . (fi,fj) = fi ^ fj ) )

thus dom f = [#] [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] by FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( rng f = [#] (TopSpaceMetr (Euclid (i + j))) & f is one-to-one & f is continuous & f " is continuous & ( for fi, fj being FinSequence st [fi,fj] in dom f holds

f . (fi,fj) = fi ^ fj ) )

thus A6: rng f = [#] (TopSpaceMetr (Euclid (i + j))) :: thesis: ( f is one-to-one & f is continuous & f " is continuous & ( for fi, fj being FinSequence st [fi,fj] in dom f holds

f . (fi,fj) = fi ^ fj ) )

proof

thus A11:
f is one-to-one
:: thesis: ( f is continuous & f " is continuous & ( for fi, fj being FinSequence st [fi,fj] in dom f holds
thus
rng f c= [#] (TopSpaceMetr (Euclid (i + j)))
; :: according to XBOOLE_0:def 10 :: thesis: [#] (TopSpaceMetr (Euclid (i + j))) c= rng f

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [#] (TopSpaceMetr (Euclid (i + j))) or y in rng f )

assume y in [#] (TopSpaceMetr (Euclid (i + j))) ; :: thesis: y in rng f

then reconsider k = y as Element of REAL (i + j) by TOPMETR:12;

len k = i + j by CARD_1:def 7;

then consider g, h being FinSequence of REAL such that

A7: ( len g = i & len h = j ) and

A8: k = g ^ h by FINSEQ_2:23;

A9: ( g in the carrier of (Euclid i) & h in the carrier of (Euclid j) ) by A7, Th16;

then [g,h] in [: the carrier of (Euclid i), the carrier of (Euclid j):] by ZFMISC_1:87;

then A10: [g,h] in dom f by FUNCT_2:def 1;

ex fi, fj being FinSequence of REAL st

( fi = g & fj = h & f . (g,h) = fi ^ fj ) by A3, A9;

hence y in rng f by A8, A10, FUNCT_1:def 3; :: thesis: verum

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [#] (TopSpaceMetr (Euclid (i + j))) or y in rng f )

assume y in [#] (TopSpaceMetr (Euclid (i + j))) ; :: thesis: y in rng f

then reconsider k = y as Element of REAL (i + j) by TOPMETR:12;

len k = i + j by CARD_1:def 7;

then consider g, h being FinSequence of REAL such that

A7: ( len g = i & len h = j ) and

A8: k = g ^ h by FINSEQ_2:23;

A9: ( g in the carrier of (Euclid i) & h in the carrier of (Euclid j) ) by A7, Th16;

then [g,h] in [: the carrier of (Euclid i), the carrier of (Euclid j):] by ZFMISC_1:87;

then A10: [g,h] in dom f by FUNCT_2:def 1;

ex fi, fj being FinSequence of REAL st

( fi = g & fj = h & f . (g,h) = fi ^ fj ) by A3, A9;

hence y in rng f by A8, A10, FUNCT_1:def 3; :: thesis: verum

f . (fi,fj) = fi ^ fj ) )

proof

A27:
for P being Subset of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) st P is open holds
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )

assume x1 in dom f ; :: thesis: ( not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )

then consider x1a, x1b being object such that

A12: x1a in the carrier of (Euclid i) and

A13: x1b in the carrier of (Euclid j) and

A14: x1 = [x1a,x1b] by A4, A1, A5, ZFMISC_1:def 2;

assume x2 in dom f ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )

then consider x2a, x2b being object such that

A15: x2a in the carrier of (Euclid i) and

A16: x2b in the carrier of (Euclid j) and

A17: x2 = [x2a,x2b] by A4, A1, A5, ZFMISC_1:def 2;

assume A18: f . x1 = f . x2 ; :: thesis: x1 = x2

consider fi1, fj1 being FinSequence of REAL such that

A19: fi1 = x1a and

A20: fj1 = x1b and

A21: f . (x1a,x1b) = fi1 ^ fj1 by A3, A12, A13;

consider fi2, fj2 being FinSequence of REAL such that

A22: fi2 = x2a and

A23: fj2 = x2b and

A24: f . (x2a,x2b) = fi2 ^ fj2 by A3, A15, A16;

len fj1 = j by A13, A20, CARD_1:def 7;

then A25: len fj1 = len fj2 by A16, A23, CARD_1:def 7;

A26: len fi1 = i by A12, A19, CARD_1:def 7;

then len fi1 = len fi2 by A15, A22, CARD_1:def 7;

then fi1 = fi2 by A14, A17, A21, A24, A25, A18, Th5;

hence x1 = x2 by A14, A17, A19, A20, A21, A22, A23, A24, A26, A25, A18, Th5; :: thesis: verum

end;assume x1 in dom f ; :: thesis: ( not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )

then consider x1a, x1b being object such that

A12: x1a in the carrier of (Euclid i) and

A13: x1b in the carrier of (Euclid j) and

A14: x1 = [x1a,x1b] by A4, A1, A5, ZFMISC_1:def 2;

assume x2 in dom f ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )

then consider x2a, x2b being object such that

A15: x2a in the carrier of (Euclid i) and

A16: x2b in the carrier of (Euclid j) and

A17: x2 = [x2a,x2b] by A4, A1, A5, ZFMISC_1:def 2;

assume A18: f . x1 = f . x2 ; :: thesis: x1 = x2

consider fi1, fj1 being FinSequence of REAL such that

A19: fi1 = x1a and

A20: fj1 = x1b and

A21: f . (x1a,x1b) = fi1 ^ fj1 by A3, A12, A13;

consider fi2, fj2 being FinSequence of REAL such that

A22: fi2 = x2a and

A23: fj2 = x2b and

A24: f . (x2a,x2b) = fi2 ^ fj2 by A3, A15, A16;

len fj1 = j by A13, A20, CARD_1:def 7;

then A25: len fj1 = len fj2 by A16, A23, CARD_1:def 7;

A26: len fi1 = i by A12, A19, CARD_1:def 7;

then len fi1 = len fi2 by A15, A22, CARD_1:def 7;

then fi1 = fi2 by A14, A17, A21, A24, A25, A18, Th5;

hence x1 = x2 by A14, A17, A19, A20, A21, A22, A23, A24, A26, A25, A18, Th5; :: thesis: verum

(f ") " P is open

proof

A56:
for P being Subset of (TopSpaceMetr (Euclid (i + j))) st P is open holds
let P be Subset of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))); :: thesis: ( P is open implies (f ") " P is open )

assume P is open ; :: thesis: (f ") " P is open

then P in the topology of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) ;

then A28: P in Family_open_set (max-Prod2 ((Euclid i),(Euclid j))) by TOPMETR:12;

A29: for x being Point of (Euclid (i + j)) st x in f .: P holds

ex r being Real st

( r > 0 & Ball (x,r) c= f .: P )

then f .: P in Family_open_set (Euclid (i + j)) by A29, PCOMPS_1:def 4;

then f .: P in the topology of (TopSpaceMetr (Euclid (i + j))) by TOPMETR:12;

hence (f ") " P in the topology of (TopSpaceMetr (Euclid (i + j))) by A6, A11, A5, TOPS_2:54; :: according to PRE_TOPC:def 2 :: thesis: verum

end;assume P is open ; :: thesis: (f ") " P is open

then P in the topology of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) ;

then A28: P in Family_open_set (max-Prod2 ((Euclid i),(Euclid j))) by TOPMETR:12;

A29: for x being Point of (Euclid (i + j)) st x in f .: P holds

ex r being Real st

( r > 0 & Ball (x,r) c= f .: P )

proof

f .: P is Subset of (Euclid (i + j))
by TOPMETR:12;
let x be Point of (Euclid (i + j)); :: thesis: ( x in f .: P implies ex r being Real st

( r > 0 & Ball (x,r) c= f .: P ) )

assume x in f .: P ; :: thesis: ex r being Real st

( r > 0 & Ball (x,r) c= f .: P )

then consider a being object such that

A30: a in the carrier of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) and

A31: a in P and

A32: x = f . a by FUNCT_2:64;

reconsider a = a as Point of (max-Prod2 ((Euclid i),(Euclid j))) by A30, TOPMETR:12;

consider r being Real such that

A33: r > 0 and

A34: Ball (a,r) c= P by A28, A31, PCOMPS_1:def 4;

take r ; :: thesis: ( r > 0 & Ball (x,r) c= f .: P )

thus r > 0 by A33; :: thesis: Ball (x,r) c= f .: P

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Ball (x,r) or b in f .: P )

assume A35: b in Ball (x,r) ; :: thesis: b in f .: P

then reconsider bb = b as Point of (Euclid (i + j)) ;

reconsider bb2 = bb, xx2 = x as Element of REAL (i + j) ;

dist (bb,x) < r by A35, METRIC_1:11;

then |.(bb2 - xx2).| < r by EUCLID:def 6;

then A36: sqrt (Sum (sqr (abs (bb2 - xx2)))) < r by EUCLID:25;

reconsider k = bb as Element of REAL (i + j) ;

len k = i + j by CARD_1:def 7;

then consider g, h being FinSequence of REAL such that

A37: len g = i and

A38: len h = j and

A39: k = g ^ h by FINSEQ_2:23;

reconsider hh = h as Point of (Euclid j) by A38, Th16;

reconsider gg = g as Point of (Euclid i) by A37, Th16;

consider g, h being FinSequence of REAL such that

A40: g = gg and

A41: h = hh and

A42: f . (gg,hh) = g ^ h by A3;

reconsider gg2 = gg, a12 = a `1 as Element of REAL i ;

A43: ( max ((dist (gg,(a `1))),(dist (hh,(a `2)))) = dist (gg,(a `1)) or max ((dist (gg,(a `1))),(dist (hh,(a `2)))) = dist (hh,(a `2)) ) by XXREAL_0:16;

consider p, q being object such that

A44: p in the carrier of (Euclid i) and

A45: q in the carrier of (Euclid j) and

A46: a = [p,q] by A4, ZFMISC_1:def 2;

reconsider q = q as Element of the carrier of (Euclid j) by A45;

reconsider p = p as Element of the carrier of (Euclid i) by A44;

consider fi, fj being FinSequence of REAL such that

A47: fi = p and

A48: fj = q and

A49: f . (p,q) = fi ^ fj by A3;

A50: ( len fi = i & len fj = j ) by A47, A48, CARD_1:def 7;

( len g = i & len h = j ) by A40, A41, CARD_1:def 7;

then sqrt (Sum (sqr ((abs (g - fi)) ^ (abs (h - fj))))) < r by A32, A39, A46, A49, A40, A41, A50, A36, Th15;

then sqrt (Sum ((sqr (abs (g - fi))) ^ (sqr (abs (h - fj))))) < r by Th10;

then A51: sqrt ((Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj))))) < r by RVSUM_1:75;

reconsider hh2 = hh, a22 = a `2 as Element of REAL j ;

A52: a22 = q by A46;

0 <= Sum (sqr (abs (g - fi))) by RVSUM_1:86;

then ( 0 <= Sum (sqr (abs (hh2 - a22))) & (Sum (sqr (abs (hh2 - a22)))) + 0 <= (Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj)))) ) by A48, A41, A52, RVSUM_1:86, XREAL_1:7;

then sqrt (Sum (sqr (abs (hh2 - a22)))) <= sqrt ((Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj))))) by SQUARE_1:26;

then sqrt (Sum (sqr (abs (hh2 - a22)))) < r by A51, XXREAL_0:2;

then |.(hh2 - a22).| < r by EUCLID:25;

then A53: (Pitag_dist j) . (hh2,a22) < r by EUCLID:def 6;

A54: a12 = p by A46;

0 <= Sum (sqr (abs (h - fj))) by RVSUM_1:86;

then ( 0 <= Sum (sqr (abs (gg2 - a12))) & (Sum (sqr (abs (gg2 - a12)))) + 0 <= (Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj)))) ) by A47, A40, A54, RVSUM_1:86, XREAL_1:7;

then sqrt (Sum (sqr (abs (gg2 - a12)))) <= sqrt ((Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj))))) by SQUARE_1:26;

then sqrt (Sum (sqr (abs (gg2 - a12)))) < r by A51, XXREAL_0:2;

then |.(gg2 - a12).| < r by EUCLID:25;

then A55: (Pitag_dist i) . (gg2,a12) < r by EUCLID:def 6;

dist ([gg,hh],[(a `1),(a `2)]) = max ((dist (gg,(a `1))),(dist (hh,(a `2)))) by Th18;

then dist ([gg,hh],a) < r by A4, A55, A53, A43, MCART_1:21;

then [g,h] in Ball (a,r) by A40, A41, METRIC_1:11;

then [g,h] in P by A34;

hence b in f .: P by A39, A40, A41, A42, FUNCT_2:35; :: thesis: verum

end;( r > 0 & Ball (x,r) c= f .: P ) )

assume x in f .: P ; :: thesis: ex r being Real st

( r > 0 & Ball (x,r) c= f .: P )

then consider a being object such that

A30: a in the carrier of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) and

A31: a in P and

A32: x = f . a by FUNCT_2:64;

reconsider a = a as Point of (max-Prod2 ((Euclid i),(Euclid j))) by A30, TOPMETR:12;

consider r being Real such that

A33: r > 0 and

A34: Ball (a,r) c= P by A28, A31, PCOMPS_1:def 4;

take r ; :: thesis: ( r > 0 & Ball (x,r) c= f .: P )

thus r > 0 by A33; :: thesis: Ball (x,r) c= f .: P

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Ball (x,r) or b in f .: P )

assume A35: b in Ball (x,r) ; :: thesis: b in f .: P

then reconsider bb = b as Point of (Euclid (i + j)) ;

reconsider bb2 = bb, xx2 = x as Element of REAL (i + j) ;

dist (bb,x) < r by A35, METRIC_1:11;

then |.(bb2 - xx2).| < r by EUCLID:def 6;

then A36: sqrt (Sum (sqr (abs (bb2 - xx2)))) < r by EUCLID:25;

reconsider k = bb as Element of REAL (i + j) ;

len k = i + j by CARD_1:def 7;

then consider g, h being FinSequence of REAL such that

A37: len g = i and

A38: len h = j and

A39: k = g ^ h by FINSEQ_2:23;

reconsider hh = h as Point of (Euclid j) by A38, Th16;

reconsider gg = g as Point of (Euclid i) by A37, Th16;

consider g, h being FinSequence of REAL such that

A40: g = gg and

A41: h = hh and

A42: f . (gg,hh) = g ^ h by A3;

reconsider gg2 = gg, a12 = a `1 as Element of REAL i ;

A43: ( max ((dist (gg,(a `1))),(dist (hh,(a `2)))) = dist (gg,(a `1)) or max ((dist (gg,(a `1))),(dist (hh,(a `2)))) = dist (hh,(a `2)) ) by XXREAL_0:16;

consider p, q being object such that

A44: p in the carrier of (Euclid i) and

A45: q in the carrier of (Euclid j) and

A46: a = [p,q] by A4, ZFMISC_1:def 2;

reconsider q = q as Element of the carrier of (Euclid j) by A45;

reconsider p = p as Element of the carrier of (Euclid i) by A44;

consider fi, fj being FinSequence of REAL such that

A47: fi = p and

A48: fj = q and

A49: f . (p,q) = fi ^ fj by A3;

A50: ( len fi = i & len fj = j ) by A47, A48, CARD_1:def 7;

( len g = i & len h = j ) by A40, A41, CARD_1:def 7;

then sqrt (Sum (sqr ((abs (g - fi)) ^ (abs (h - fj))))) < r by A32, A39, A46, A49, A40, A41, A50, A36, Th15;

then sqrt (Sum ((sqr (abs (g - fi))) ^ (sqr (abs (h - fj))))) < r by Th10;

then A51: sqrt ((Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj))))) < r by RVSUM_1:75;

reconsider hh2 = hh, a22 = a `2 as Element of REAL j ;

A52: a22 = q by A46;

0 <= Sum (sqr (abs (g - fi))) by RVSUM_1:86;

then ( 0 <= Sum (sqr (abs (hh2 - a22))) & (Sum (sqr (abs (hh2 - a22)))) + 0 <= (Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj)))) ) by A48, A41, A52, RVSUM_1:86, XREAL_1:7;

then sqrt (Sum (sqr (abs (hh2 - a22)))) <= sqrt ((Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj))))) by SQUARE_1:26;

then sqrt (Sum (sqr (abs (hh2 - a22)))) < r by A51, XXREAL_0:2;

then |.(hh2 - a22).| < r by EUCLID:25;

then A53: (Pitag_dist j) . (hh2,a22) < r by EUCLID:def 6;

A54: a12 = p by A46;

0 <= Sum (sqr (abs (h - fj))) by RVSUM_1:86;

then ( 0 <= Sum (sqr (abs (gg2 - a12))) & (Sum (sqr (abs (gg2 - a12)))) + 0 <= (Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj)))) ) by A47, A40, A54, RVSUM_1:86, XREAL_1:7;

then sqrt (Sum (sqr (abs (gg2 - a12)))) <= sqrt ((Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj))))) by SQUARE_1:26;

then sqrt (Sum (sqr (abs (gg2 - a12)))) < r by A51, XXREAL_0:2;

then |.(gg2 - a12).| < r by EUCLID:25;

then A55: (Pitag_dist i) . (gg2,a12) < r by EUCLID:def 6;

dist ([gg,hh],[(a `1),(a `2)]) = max ((dist (gg,(a `1))),(dist (hh,(a `2)))) by Th18;

then dist ([gg,hh],a) < r by A4, A55, A53, A43, MCART_1:21;

then [g,h] in Ball (a,r) by A40, A41, METRIC_1:11;

then [g,h] in P by A34;

hence b in f .: P by A39, A40, A41, A42, FUNCT_2:35; :: thesis: verum

then f .: P in Family_open_set (Euclid (i + j)) by A29, PCOMPS_1:def 4;

then f .: P in the topology of (TopSpaceMetr (Euclid (i + j))) by TOPMETR:12;

hence (f ") " P in the topology of (TopSpaceMetr (Euclid (i + j))) by A6, A11, A5, TOPS_2:54; :: according to PRE_TOPC:def 2 :: thesis: verum

f " P is open

proof

[#] (TopSpaceMetr (Euclid (i + j))) <> {}
;
let P be Subset of (TopSpaceMetr (Euclid (i + j))); :: thesis: ( P is open implies f " P is open )

assume P is open ; :: thesis: f " P is open

then P in the topology of (TopSpaceMetr (Euclid (i + j))) ;

then A57: P in Family_open_set (Euclid (i + j)) by TOPMETR:12;

A58: for x being Point of (max-Prod2 ((Euclid i),(Euclid j))) st x in f " P holds

ex r being Real st

( r > 0 & Ball (x,r) c= f " P )

then f " P in Family_open_set (max-Prod2 ((Euclid i),(Euclid j))) by A58, PCOMPS_1:def 4;

hence f " P in the topology of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] by A5, TOPMETR:12; :: according to PRE_TOPC:def 2 :: thesis: verum

end;assume P is open ; :: thesis: f " P is open

then P in the topology of (TopSpaceMetr (Euclid (i + j))) ;

then A57: P in Family_open_set (Euclid (i + j)) by TOPMETR:12;

A58: for x being Point of (max-Prod2 ((Euclid i),(Euclid j))) st x in f " P holds

ex r being Real st

( r > 0 & Ball (x,r) c= f " P )

proof

f " P is Subset of (max-Prod2 ((Euclid i),(Euclid j)))
by A5, TOPMETR:12;
let x be Point of (max-Prod2 ((Euclid i),(Euclid j))); :: thesis: ( x in f " P implies ex r being Real st

( r > 0 & Ball (x,r) c= f " P ) )

assume A59: x in f " P ; :: thesis: ex r being Real st

( r > 0 & Ball (x,r) c= f " P )

then f . x in the carrier of (TopSpaceMetr (Euclid (i + j))) by FUNCT_2:5;

then reconsider fx = f . x as Point of (Euclid (i + j)) by TOPMETR:12;

f . x in P by A59, FUNCT_2:38;

then consider r being Real such that

A60: r > 0 and

A61: Ball (fx,r) c= P by A57, PCOMPS_1:def 4;

take r1 = r / 2; :: thesis: ( r1 > 0 & Ball (x,r1) c= f " P )

thus r1 > 0 by A60, XREAL_1:139; :: thesis: Ball (x,r1) c= f " P

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Ball (x,r1) or b in f " P )

assume A62: b in Ball (x,r1) ; :: thesis: b in f " P

then reconsider bb = b as Point of (max-Prod2 ((Euclid i),(Euclid j))) ;

A63: dist (bb,x) < r1 by A62, METRIC_1:11;

bb in the carrier of (max-Prod2 ((Euclid i),(Euclid j))) ;

then A64: bb in the carrier of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) by TOPMETR:12;

then f . bb in the carrier of (TopSpaceMetr (Euclid (i + j))) by FUNCT_2:5;

then reconsider fb = f . b as Point of (Euclid (i + j)) by TOPMETR:12;

reconsider fbb = fb, fxx = fx as Element of REAL (i + j) ;

consider b1, x1 being Point of (Euclid i), b2, x2 being Point of (Euclid j) such that

A65: ( bb = [b1,b2] & x = [x1,x2] ) and

the distance of (max-Prod2 ((Euclid i),(Euclid j))) . (bb,x) = max (( the distance of (Euclid i) . (b1,x1)),( the distance of (Euclid j) . (b2,x2))) by Def1;

A66: dist ([b1,b2],[x1,x2]) = max ((dist (b1,x1)),(dist (b2,x2))) by Th18;

dist (b2,x2) <= max ((dist (b1,x1)),(dist (b2,x2))) by XXREAL_0:25;

then A67: dist (b2,x2) < r1 by A65, A66, A63, XXREAL_0:2;

reconsider x2i = x2, b2i = b2 as Element of REAL j ;

reconsider b1i = b1, x1i = x1 as Element of REAL i ;

consider b1f, b2f being FinSequence of REAL such that

A68: ( b1f = b1 & b2f = b2 ) and

A69: f . (b1,b2) = b1f ^ b2f by A3;

A70: ( len b1f = i & len b2f = j ) by A68, CARD_1:def 7;

dist (b1,x1) <= max ((dist (b1,x1)),(dist (b2,x2))) by XXREAL_0:25;

then dist (b1,x1) < r1 by A65, A66, A63, XXREAL_0:2;

then A71: ((Pitag_dist i) . (b1i,x1i)) + ((Pitag_dist j) . (b2i,x2i)) < r1 + r1 by A67, XREAL_1:8;

( 0 <= Sum (sqr (b1i - x1i)) & 0 <= Sum (sqr (b2i - x2i)) ) by RVSUM_1:86;

then sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) <= |.(b1i - x1i).| + (sqrt (Sum (sqr (b2i - x2i)))) by SQUARE_1:59;

then sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) <= ((Pitag_dist i) . (b1i,x1i)) + |.(b2i - x2i).| by EUCLID:def 6;

then A72: sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) <= ((Pitag_dist i) . (b1i,x1i)) + ((Pitag_dist j) . (b2i,x2i)) by EUCLID:def 6;

consider x1f, x2f being FinSequence of REAL such that

A73: ( x1f = x1 & x2f = x2 ) and

A74: f . (x1,x2) = x1f ^ x2f by A3;

A75: ( len x1f = i & len x2f = j ) by A73, CARD_1:def 7;

(Pitag_dist (i + j)) . (fbb,fxx) = |.(fbb - fxx).| by EUCLID:def 6

.= sqrt (Sum (sqr (abs (fbb - fxx)))) by EUCLID:25

.= sqrt (Sum (sqr ((abs (b1i - x1i)) ^ (abs (b2i - x2i))))) by A65, A68, A69, A73, A74, A70, A75, Th15

.= sqrt (Sum ((sqr (abs (b1i - x1i))) ^ (sqr (abs (b2i - x2i))))) by Th10

.= sqrt ((Sum (sqr (abs (b1i - x1i)))) + (Sum (sqr (abs (b2i - x2i))))) by RVSUM_1:75

.= sqrt ((Sum (sqr (abs (b1i - x1i)))) + (Sum (sqr (b2i - x2i)))) by EUCLID:25

.= sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) by EUCLID:25 ;

then dist (fb,fx) < r by A72, A71, XXREAL_0:2;

then f . b in Ball (fx,r) by METRIC_1:11;

hence b in f " P by A61, A64, FUNCT_2:38; :: thesis: verum

end;( r > 0 & Ball (x,r) c= f " P ) )

assume A59: x in f " P ; :: thesis: ex r being Real st

( r > 0 & Ball (x,r) c= f " P )

then f . x in the carrier of (TopSpaceMetr (Euclid (i + j))) by FUNCT_2:5;

then reconsider fx = f . x as Point of (Euclid (i + j)) by TOPMETR:12;

f . x in P by A59, FUNCT_2:38;

then consider r being Real such that

A60: r > 0 and

A61: Ball (fx,r) c= P by A57, PCOMPS_1:def 4;

take r1 = r / 2; :: thesis: ( r1 > 0 & Ball (x,r1) c= f " P )

thus r1 > 0 by A60, XREAL_1:139; :: thesis: Ball (x,r1) c= f " P

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Ball (x,r1) or b in f " P )

assume A62: b in Ball (x,r1) ; :: thesis: b in f " P

then reconsider bb = b as Point of (max-Prod2 ((Euclid i),(Euclid j))) ;

A63: dist (bb,x) < r1 by A62, METRIC_1:11;

bb in the carrier of (max-Prod2 ((Euclid i),(Euclid j))) ;

then A64: bb in the carrier of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) by TOPMETR:12;

then f . bb in the carrier of (TopSpaceMetr (Euclid (i + j))) by FUNCT_2:5;

then reconsider fb = f . b as Point of (Euclid (i + j)) by TOPMETR:12;

reconsider fbb = fb, fxx = fx as Element of REAL (i + j) ;

consider b1, x1 being Point of (Euclid i), b2, x2 being Point of (Euclid j) such that

A65: ( bb = [b1,b2] & x = [x1,x2] ) and

the distance of (max-Prod2 ((Euclid i),(Euclid j))) . (bb,x) = max (( the distance of (Euclid i) . (b1,x1)),( the distance of (Euclid j) . (b2,x2))) by Def1;

A66: dist ([b1,b2],[x1,x2]) = max ((dist (b1,x1)),(dist (b2,x2))) by Th18;

dist (b2,x2) <= max ((dist (b1,x1)),(dist (b2,x2))) by XXREAL_0:25;

then A67: dist (b2,x2) < r1 by A65, A66, A63, XXREAL_0:2;

reconsider x2i = x2, b2i = b2 as Element of REAL j ;

reconsider b1i = b1, x1i = x1 as Element of REAL i ;

consider b1f, b2f being FinSequence of REAL such that

A68: ( b1f = b1 & b2f = b2 ) and

A69: f . (b1,b2) = b1f ^ b2f by A3;

A70: ( len b1f = i & len b2f = j ) by A68, CARD_1:def 7;

dist (b1,x1) <= max ((dist (b1,x1)),(dist (b2,x2))) by XXREAL_0:25;

then dist (b1,x1) < r1 by A65, A66, A63, XXREAL_0:2;

then A71: ((Pitag_dist i) . (b1i,x1i)) + ((Pitag_dist j) . (b2i,x2i)) < r1 + r1 by A67, XREAL_1:8;

( 0 <= Sum (sqr (b1i - x1i)) & 0 <= Sum (sqr (b2i - x2i)) ) by RVSUM_1:86;

then sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) <= |.(b1i - x1i).| + (sqrt (Sum (sqr (b2i - x2i)))) by SQUARE_1:59;

then sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) <= ((Pitag_dist i) . (b1i,x1i)) + |.(b2i - x2i).| by EUCLID:def 6;

then A72: sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) <= ((Pitag_dist i) . (b1i,x1i)) + ((Pitag_dist j) . (b2i,x2i)) by EUCLID:def 6;

consider x1f, x2f being FinSequence of REAL such that

A73: ( x1f = x1 & x2f = x2 ) and

A74: f . (x1,x2) = x1f ^ x2f by A3;

A75: ( len x1f = i & len x2f = j ) by A73, CARD_1:def 7;

(Pitag_dist (i + j)) . (fbb,fxx) = |.(fbb - fxx).| by EUCLID:def 6

.= sqrt (Sum (sqr (abs (fbb - fxx)))) by EUCLID:25

.= sqrt (Sum (sqr ((abs (b1i - x1i)) ^ (abs (b2i - x2i))))) by A65, A68, A69, A73, A74, A70, A75, Th15

.= sqrt (Sum ((sqr (abs (b1i - x1i))) ^ (sqr (abs (b2i - x2i))))) by Th10

.= sqrt ((Sum (sqr (abs (b1i - x1i)))) + (Sum (sqr (abs (b2i - x2i))))) by RVSUM_1:75

.= sqrt ((Sum (sqr (abs (b1i - x1i)))) + (Sum (sqr (b2i - x2i)))) by EUCLID:25

.= sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) by EUCLID:25 ;

then dist (fb,fx) < r by A72, A71, XXREAL_0:2;

then f . b in Ball (fx,r) by METRIC_1:11;

hence b in f " P by A61, A64, FUNCT_2:38; :: thesis: verum

then f " P in Family_open_set (max-Prod2 ((Euclid i),(Euclid j))) by A58, PCOMPS_1:def 4;

hence f " P in the topology of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] by A5, TOPMETR:12; :: according to PRE_TOPC:def 2 :: thesis: verum

hence f is continuous by A56, TOPS_2:43; :: thesis: ( f " is continuous & ( for fi, fj being FinSequence st [fi,fj] in dom f holds

f . (fi,fj) = fi ^ fj ) )

[#] (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) <> {} ;

hence f " is continuous by A27, A5, TOPS_2:43; :: thesis: for fi, fj being FinSequence st [fi,fj] in dom f holds

f . (fi,fj) = fi ^ fj

let fi, fj be FinSequence; :: thesis: ( [fi,fj] in dom f implies f . (fi,fj) = fi ^ fj )

assume A76: [fi,fj] in dom f ; :: thesis: f . (fi,fj) = fi ^ fj

then reconsider Fi = fi as Element of the carrier of (Euclid i) by A1, A5, A4, ZFMISC_1:87;

reconsider Fj = fj as Element of the carrier of (Euclid j) by A76, A1, A5, A4, ZFMISC_1:87;

S

hence f . (fi,fj) = fi ^ fj ; :: thesis: verum