:: TOPREAL7 semantic presentation

begin


theorem Th1: :: TOPREAL7:1
for a, b, c, d being Real holds max ((a + c),(b + d)) <= (max (a,b)) + (max (c,d))
proof
let a, b, c, d be Real; ::_thesis: max ((a + c),(b + d)) <= (max (a,b)) + (max (c,d))
 ( b <= max (a,b) & d <= max (c,d) ) by XXREAL_0:25;
then A1: b + d <= (max (a,b)) + (max (c,d)) by XREAL_1:7;
 ( a <= max (a,b) & c <= max (c,d) ) by XXREAL_0:25;
then  a + c <= (max (a,b)) + (max (c,d)) by XREAL_1:7;
hence  max ((a + c),(b + d)) <= (max (a,b)) + (max (c,d)) by A1, XXREAL_0:28; ::_thesis: verum
end;

theorem Th2: :: TOPREAL7:2
for a, b, c, d, e, f being Real st a <= b + c & d <= e + f holds
max (a,d) <= (max (b,e)) + (max (c,f))
proof
let a, b, c, d, e, f be Real; ::_thesis: ( a <= b + c & d <= e + f implies max (a,d) <= (max (b,e)) + (max (c,f)) )
assume  ( a <= b + c & d <= e + f ) ; ::_thesis: max (a,d) <= (max (b,e)) + (max (c,f))
then A1: max (a,d) <= max ((b + c),(e + f)) by XXREAL_0:26;
 max ((b + c),(e + f)) <= (max (b,e)) + (max (c,f)) by Th1;
hence  max (a,d) <= (max (b,e)) + (max (c,f)) by A1, XXREAL_0:2; ::_thesis: verum
end;

theorem :: TOPREAL7:3
for f, g being FinSequence holds dom g c= dom (f ^ g)
proof
let f, g be FinSequence; ::_thesis: dom g c= dom (f ^ g)
 len g <= (len f) + (len g) by NAT_1:11;
then  Seg (len g) c= Seg ((len f) + (len g)) by FINSEQ_1:5;
then  dom g c= Seg ((len f) + (len g)) by FINSEQ_1:def_3;
hence  dom g c= dom (f ^ g) by FINSEQ_1:def_7; ::_thesis: verum
end;

theorem Th4: :: TOPREAL7:4
for i being Nat
for f, g being FinSequence st len f < i & i <= (len f) + (len g) holds
i - (len f) in dom g
proof
let i be Nat; ::_thesis: for f, g being FinSequence st len f < i & i <= (len f) + (len g) holds
i - (len f) in dom g
let f, g be FinSequence; ::_thesis: ( len f < i & i <= (len f) + (len g) implies i - (len f) in dom g )
assume that
A1: len f < i and
A2: i <= (len f) + (len g) ; ::_thesis: i - (len f) in dom g
A3: i - (len f) is Element of NAT by A1, INT_1:5;
A4: i - (len f) <= ((len f) + (len g)) - (len f) by A2, XREAL_1:9;
 i - (len f) > (len f) - (len f) by A1, XREAL_1:14;
then  1 <= i - (len f) by A3, NAT_1:14;
hence  i - (len f) in dom g by A3, A4, FINSEQ_3:25; ::_thesis: verum
end;

theorem Th5: :: TOPREAL7:5
for f, g, h, k being FinSequence st f ^ g = h ^ k & len f = len h & len g = len k holds
( f = h & g = k )
proof
let f, g, h, k be FinSequence; ::_thesis: ( f ^ g = h ^ k & len f = len h & len g = len k implies ( f = h & g = k ) )
assume that
A1: f ^ g = h ^ k and
A2: len f = len h and
A3: len g = len k ; ::_thesis: ( f = h & g = k )
A4: for i being Nat st 1 <= i & i <= len f holds
f . i = h . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies f . i = h . i )
assume A5: ( 1 <= i & i <= len f ) ; ::_thesis: f . i = h . i
then A6: i in dom h by A2, FINSEQ_3:25;
 i in dom f by A5, FINSEQ_3:25;
hence f . i = (f ^ g) . i by FINSEQ_1:def_7
.= h . i by A1, A6, FINSEQ_1:def_7 ;
::_thesis: verum
end;
 for i being Nat st 1 <= i & i <= len g holds
g . i = k . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len g implies g . i = k . i )
assume A7: ( 1 <= i & i <= len g ) ; ::_thesis: g . i = k . i
then A8: i in dom k by A3, FINSEQ_3:25;
 i in dom g by A7, FINSEQ_3:25;
hence g . i = (f ^ g) . ((len f) + i) by FINSEQ_1:def_7
.= k . i by A1, A2, A8, FINSEQ_1:def_7 ;
::_thesis: verum
end;
hence  ( f = h & g = k ) by A2, A3, A4, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th6: :: TOPREAL7:6
for f, g being FinSequence of REAL st ( len f = len g or dom f = dom g ) holds
( len (f + g) = len f & dom (f + g) = dom f )
proof
let f, g be FinSequence of REAL ; ::_thesis: ( ( len f = len g or dom f = dom g ) implies ( len (f + g) = len f & dom (f + g) = dom f ) )
reconsider f1 = f as Element of (len f) -tuples_on REAL by FINSEQ_2:92;
assume  ( len f = len g or dom f = dom g ) ; ::_thesis: ( len (f + g) = len f & dom (f + g) = dom f )
then  len f = len g by FINSEQ_3:29;
then reconsider g1 = g as Element of (len f) -tuples_on REAL by FINSEQ_2:92;
 f1 + g1 is Element of (len f) -tuples_on REAL ;
hence  len (f + g) = len f by CARD_1:def_7; ::_thesis: dom (f + g) = dom f
hence  dom (f + g) = dom f by FINSEQ_3:29; ::_thesis: verum
end;

theorem Th7: :: TOPREAL7:7
for f, g being FinSequence of REAL st ( len f = len g or dom f = dom g ) holds
( len (f - g) = len f & dom (f - g) = dom f )
proof
let f, g be FinSequence of REAL ; ::_thesis: ( ( len f = len g or dom f = dom g ) implies ( len (f - g) = len f & dom (f - g) = dom f ) )
reconsider f1 = f as Element of (len f) -tuples_on REAL by FINSEQ_2:92;
assume  ( len f = len g or dom f = dom g ) ; ::_thesis: ( len (f - g) = len f & dom (f - g) = dom f )
then  len f = len g by FINSEQ_3:29;
then reconsider g1 = g as Element of (len f) -tuples_on REAL by FINSEQ_2:92;
 f1 - g1 is Element of (len f) -tuples_on REAL ;
hence  len (f - g) = len f by CARD_1:def_7; ::_thesis: dom (f - g) = dom f
hence  dom (f - g) = dom f by FINSEQ_3:29; ::_thesis: verum
end;

theorem Th8: :: TOPREAL7:8
for f being FinSequence of REAL holds
( len f = len (sqr f) & dom f = dom (sqr f) ) by RVSUM_1:143;

theorem Th9: :: TOPREAL7:9
for f being FinSequence of REAL holds
( len f = len (abs f) & dom f = dom (abs f) )
proof
let f be FinSequence of REAL ; ::_thesis: ( len f = len (abs f) & dom f = dom (abs f) )
 ( rng f c= REAL & dom absreal = REAL ) by FUNCT_2:def_1;
hence  len f = len (abs f) by FINSEQ_2:29; ::_thesis: dom f = dom (abs f)
hence  dom f = dom (abs f) by FINSEQ_3:29; ::_thesis: verum
end;

theorem Th10: :: TOPREAL7:10
for f, g being FinSequence of REAL holds sqr (f ^ g) = (sqr f) ^ (sqr g) by RVSUM_1:144;

theorem :: TOPREAL7:11
for f, g being FinSequence of REAL holds abs (f ^ g) = (abs f) ^ (abs g)
proof
let f, g be FinSequence of REAL ; ::_thesis: abs (f ^ g) = (abs f) ^ (abs g)
A1: ( len g = len (abs g) & len (f ^ g) = (len f) + (len g) ) by Th9, FINSEQ_1:22;
A2: len (abs (f ^ g)) = len (f ^ g) by Th9;
A3: len f = len (abs f) by Th9;
A4: for i being Nat st 1 <= i & i <= len (abs (f ^ g)) holds
(abs (f ^ g)) . i = ((abs f) ^ (abs g)) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (abs (f ^ g)) implies (abs (f ^ g)) . i = ((abs f) ^ (abs g)) . i )
assume that
A5: 1 <= i and
A6: i <= len (abs (f ^ g)) ; ::_thesis: (abs (f ^ g)) . i = ((abs f) ^ (abs g)) . i
reconsider i1 = i as Element of NAT by ORDINAL1:def_12;
A7: i in dom (f ^ g) by A2, A5, A6, FINSEQ_3:25;
percases ( i in dom f or not i in dom f ) ;
supposeA8: i in dom f ; ::_thesis: (abs (f ^ g)) . i = ((abs f) ^ (abs g)) . i
then A9: i in dom (abs f) by Th9;
thus (abs (f ^ g)) . i = absreal . ((f ^ g) . i) by A7, FUNCT_1:13
.= absreal . (f . i) by A8, FINSEQ_1:def_7
.= abs (f . i1) by EUCLID:def_2
.= (abs f) . i1 by A9, TOPREAL6:12
.= ((abs f) ^ (abs g)) . i by A9, FINSEQ_1:def_7 ; ::_thesis: verum
end;
suppose not i in dom f ; ::_thesis: (abs (f ^ g)) . i = ((abs f) ^ (abs g)) . i
then A10: len f < i by A5, FINSEQ_3:25;
then reconsider j = i1 - (len f) as Element of NAT by INT_1:5;
A11: i <= len (f ^ g) by A6, Th9;
then A12: j in dom (abs g) by A1, A10, Th4;
A13: i <= len ((abs f) ^ (abs g)) by A3, A1, A2, A6, FINSEQ_1:22;
thus (abs (f ^ g)) . i = absreal . ((f ^ g) . i) by A7, FUNCT_1:13
.= absreal . (g . j) by A10, A11, FINSEQ_1:24
.= abs (g . j) by EUCLID:def_2
.= (abs g) . j by A12, TOPREAL6:12
.= ((abs f) ^ (abs g)) . i by A3, A10, A13, FINSEQ_1:24 ; ::_thesis: verum
end;
end;
end;
 len (abs (f ^ g)) = len ((abs f) ^ (abs g)) by A3, A1, A2, FINSEQ_1:22;
hence  abs (f ^ g) = (abs f) ^ (abs g) by A4, FINSEQ_1:14; ::_thesis: verum
end;

theorem :: TOPREAL7:12
for f, h, g, k being FinSequence of REAL st len f = len h & len g = len k holds
sqr ((f ^ g) + (h ^ k)) = (sqr (f + h)) ^ (sqr (g + k))
proof
let f, h, g, k be FinSequence of REAL ; ::_thesis: ( len f = len h & len g = len k implies sqr ((f ^ g) + (h ^ k)) = (sqr (f + h)) ^ (sqr (g + k)) )
assume that
A1: len f = len h and
A2: len g = len k ; ::_thesis: sqr ((f ^ g) + (h ^ k)) = (sqr (f + h)) ^ (sqr (g + k))
A3: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
A4: len (h ^ k) = (len h) + (len k) by FINSEQ_1:22;
A5: len (sqr ((f ^ g) + (h ^ k))) = len ((f ^ g) + (h ^ k)) by Th8
.= len (f ^ g) by A1, A2, A3, A4, Th6
.= (len (f + h)) + (len g) by A1, A3, Th6
.= (len (f + h)) + (len (g + k)) by A2, Th6
.= (len (sqr (f + h))) + (len (g + k)) by Th8
.= (len (sqr (f + h))) + (len (sqr (g + k))) by Th8
.= len ((sqr (f + h)) ^ (sqr (g + k))) by FINSEQ_1:22 ;
 for i being Nat st 1 <= i & i <= len (sqr ((f ^ g) + (h ^ k))) holds
(sqr ((f ^ g) + (h ^ k))) . i = ((sqr (f + h)) ^ (sqr (g + k))) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (sqr ((f ^ g) + (h ^ k))) implies (sqr ((f ^ g) + (h ^ k))) . i = ((sqr (f + h)) ^ (sqr (g + k))) . i )
assume that
A6: 1 <= i and
A7: i <= len (sqr ((f ^ g) + (h ^ k))) ; ::_thesis: (sqr ((f ^ g) + (h ^ k))) . i = ((sqr (f + h)) ^ (sqr (g + k))) . i
 i in dom (sqr ((f ^ g) + (h ^ k))) by A6, A7, FINSEQ_3:25;
then A8: i in dom ((f ^ g) + (h ^ k)) by Th8;
percases ( i in dom f or not i in dom f ) ;
supposeA9: i in dom f ; ::_thesis: (sqr ((f ^ g) + (h ^ k))) . i = ((sqr (f + h)) ^ (sqr (g + k))) . i
then A10: i in dom (f + h) by A1, Th6;
then A11: i in dom (sqr (f + h)) by Th8;
A12: i in dom h by A1, A9, FINSEQ_3:29;
thus (sqr ((f ^ g) + (h ^ k))) . i = (((f ^ g) + (h ^ k)) . i) ^2 by VALUED_1:11
.= (((f ^ g) . i) + ((h ^ k) . i)) ^2 by A8, VALUED_1:def_1
.= ((f . i) + ((h ^ k) . i)) ^2 by A9, FINSEQ_1:def_7
.= ((f . i) + (h . i)) ^2 by A12, FINSEQ_1:def_7
.= ((f + h) . i) ^2 by A10, VALUED_1:def_1
.= (sqr (f + h)) . i by VALUED_1:11
.= ((sqr (f + h)) ^ (sqr (g + k))) . i by A11, FINSEQ_1:def_7 ; ::_thesis: verum
end;
suppose not i in dom f ; ::_thesis: (sqr ((f ^ g) + (h ^ k))) . i = ((sqr (f + h)) ^ (sqr (g + k))) . i
then A13: len f < i by A6, FINSEQ_3:25;
then reconsider j = i - (len f) as Element of NAT by INT_1:5;
A14: len (f + h) < i by A1, A13, Th6;
then A15: len (sqr (f + h)) < i by Th8;
 i <= len ((f ^ g) + (h ^ k)) by A7, Th8;
then A16: i <= len (f ^ g) by A1, A2, A3, A4, Th6;
then  i <= (len (f + h)) + (len g) by A1, A3, Th6;
then  i <= (len (f + h)) + (len (g + k)) by A2, Th6;
then  i - (len (f + h)) in dom (g + k) by A14, Th4;
then A17: j in dom (g + k) by A1, Th6;
 len f = len (f + h) by A1, Th6;
then A18: j = i - (len (sqr (f + h))) by Th8;
thus (sqr ((f ^ g) + (h ^ k))) . i = (((f ^ g) + (h ^ k)) . i) ^2 by VALUED_1:11
.= (((f ^ g) . i) + ((h ^ k) . i)) ^2 by A8, VALUED_1:def_1
.= ((g . j) + ((h ^ k) . i)) ^2 by A13, A16, FINSEQ_1:24
.= ((g . j) + (k . j)) ^2 by A1, A2, A3, A4, A13, A16, FINSEQ_1:24
.= ((g + k) . j) ^2 by A17, VALUED_1:def_1
.= (sqr (g + k)) . j by VALUED_1:11
.= ((sqr (f + h)) ^ (sqr (g + k))) . i by A5, A7, A15, A18, FINSEQ_1:24 ; ::_thesis: verum
end;
end;
end;
hence  sqr ((f ^ g) + (h ^ k)) = (sqr (f + h)) ^ (sqr (g + k)) by A5, FINSEQ_1:14; ::_thesis: verum
end;

theorem :: TOPREAL7:13
for f, h, g, k being FinSequence of REAL st len f = len h & len g = len k holds
abs ((f ^ g) + (h ^ k)) = (abs (f + h)) ^ (abs (g + k))
proof
let f, h, g, k be FinSequence of REAL ; ::_thesis: ( len f = len h & len g = len k implies abs ((f ^ g) + (h ^ k)) = (abs (f + h)) ^ (abs (g + k)) )
assume that
A1: len f = len h and
A2: len g = len k ; ::_thesis: abs ((f ^ g) + (h ^ k)) = (abs (f + h)) ^ (abs (g + k))
A3: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
A4: len (h ^ k) = (len h) + (len k) by FINSEQ_1:22;
A5: len (abs ((f ^ g) + (h ^ k))) = len ((f ^ g) + (h ^ k)) by Th9
.= len (f ^ g) by A1, A2, A3, A4, Th6
.= (len (f + h)) + (len g) by A1, A3, Th6
.= (len (f + h)) + (len (g + k)) by A2, Th6
.= (len (abs (f + h))) + (len (g + k)) by Th9
.= (len (abs (f + h))) + (len (abs (g + k))) by Th9
.= len ((abs (f + h)) ^ (abs (g + k))) by FINSEQ_1:22 ;
 for i being Nat st 1 <= i & i <= len (abs ((f ^ g) + (h ^ k))) holds
(abs ((f ^ g) + (h ^ k))) . i = ((abs (f + h)) ^ (abs (g + k))) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (abs ((f ^ g) + (h ^ k))) implies (abs ((f ^ g) + (h ^ k))) . i = ((abs (f + h)) ^ (abs (g + k))) . i )
assume that
A6: 1 <= i and
A7: i <= len (abs ((f ^ g) + (h ^ k))) ; ::_thesis: (abs ((f ^ g) + (h ^ k))) . i = ((abs (f + h)) ^ (abs (g + k))) . i
reconsider i1 = i as Element of NAT by ORDINAL1:def_12;
A8: i in dom (abs ((f ^ g) + (h ^ k))) by A6, A7, FINSEQ_3:25;
then A9: i in dom ((f ^ g) + (h ^ k)) by Th9;
percases ( i in dom f or not i in dom f ) ;
supposeA10: i in dom f ; ::_thesis: (abs ((f ^ g) + (h ^ k))) . i = ((abs (f + h)) ^ (abs (g + k))) . i
then A11: i in dom h by A1, FINSEQ_3:29;
A12: i in dom (f + h) by A1, A10, Th6;
then A13: i in dom (abs (f + h)) by Th9;
thus (abs ((f ^ g) + (h ^ k))) . i = abs (((f ^ g) + (h ^ k)) . i1) by A8, TOPREAL6:12
.= abs (((f ^ g) . i) + ((h ^ k) . i)) by A9, VALUED_1:def_1
.= abs ((f . i) + ((h ^ k) . i)) by A10, FINSEQ_1:def_7
.= abs ((f . i) + (h . i)) by A11, FINSEQ_1:def_7
.= abs ((f + h) . i1) by A12, VALUED_1:def_1
.= (abs (f + h)) . i1 by A13, TOPREAL6:12
.= ((abs (f + h)) ^ (abs (g + k))) . i by A13, FINSEQ_1:def_7 ; ::_thesis: verum
end;
suppose not i in dom f ; ::_thesis: (abs ((f ^ g) + (h ^ k))) . i = ((abs (f + h)) ^ (abs (g + k))) . i
then A14: len f < i by A6, FINSEQ_3:25;
then reconsider j = i - (len f) as Element of NAT by INT_1:5;
A15: len (f + h) < i by A1, A14, Th6;
then A16: len (abs (f + h)) < i by Th9;
 i <= len ((f ^ g) + (h ^ k)) by A7, Th9;
then A17: i <= len (f ^ g) by A1, A2, A3, A4, Th6;
then  i <= (len (f + h)) + (len g) by A1, A3, Th6;
then  i <= (len (f + h)) + (len (g + k)) by A2, Th6;
then  i - (len (f + h)) in dom (g + k) by A15, Th4;
then A18: j in dom (g + k) by A1, Th6;
then A19: j in dom (abs (g + k)) by Th9;
 len f = len (f + h) by A1, Th6;
then A20: j = i - (len (abs (f + h))) by Th9;
thus (abs ((f ^ g) + (h ^ k))) . i = abs (((f ^ g) + (h ^ k)) . i1) by A8, TOPREAL6:12
.= abs (((f ^ g) . i) + ((h ^ k) . i)) by A9, VALUED_1:def_1
.= abs ((g . j) + ((h ^ k) . i)) by A14, A17, FINSEQ_1:24
.= abs ((g . j) + (k . j)) by A1, A2, A3, A4, A14, A17, FINSEQ_1:24
.= abs ((g + k) . j) by A18, VALUED_1:def_1
.= (abs (g + k)) . j by A19, TOPREAL6:12
.= ((abs (f + h)) ^ (abs (g + k))) . i by A5, A7, A16, A20, FINSEQ_1:24 ; ::_thesis: verum
end;
end;
end;
hence  abs ((f ^ g) + (h ^ k)) = (abs (f + h)) ^ (abs (g + k)) by A5, FINSEQ_1:14; ::_thesis: verum
end;

theorem :: TOPREAL7:14
for f, h, g, k being FinSequence of REAL st len f = len h & len g = len k holds
sqr ((f ^ g) - (h ^ k)) = (sqr (f - h)) ^ (sqr (g - k))
proof
let f, h, g, k be FinSequence of REAL ; ::_thesis: ( len f = len h & len g = len k implies sqr ((f ^ g) - (h ^ k)) = (sqr (f - h)) ^ (sqr (g - k)) )
assume that
A1: len f = len h and
A2: len g = len k ; ::_thesis: sqr ((f ^ g) - (h ^ k)) = (sqr (f - h)) ^ (sqr (g - k))
A3: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
A4: len (h ^ k) = (len h) + (len k) by FINSEQ_1:22;
A5: len (sqr ((f ^ g) - (h ^ k))) = len ((f ^ g) - (h ^ k)) by Th8
.= len (f ^ g) by A1, A2, A3, A4, Th7
.= (len (f - h)) + (len g) by A1, A3, Th7
.= (len (f - h)) + (len (g - k)) by A2, Th7
.= (len (sqr (f - h))) + (len (g - k)) by Th8
.= (len (sqr (f - h))) + (len (sqr (g - k))) by Th8
.= len ((sqr (f - h)) ^ (sqr (g - k))) by FINSEQ_1:22 ;
 for i being Nat st 1 <= i & i <= len (sqr ((f ^ g) - (h ^ k))) holds
(sqr ((f ^ g) - (h ^ k))) . i = ((sqr (f - h)) ^ (sqr (g - k))) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (sqr ((f ^ g) - (h ^ k))) implies (sqr ((f ^ g) - (h ^ k))) . i = ((sqr (f - h)) ^ (sqr (g - k))) . i )
assume that
A6: 1 <= i and
A7: i <= len (sqr ((f ^ g) - (h ^ k))) ; ::_thesis: (sqr ((f ^ g) - (h ^ k))) . i = ((sqr (f - h)) ^ (sqr (g - k))) . i
 i in dom (sqr ((f ^ g) - (h ^ k))) by A6, A7, FINSEQ_3:25;
then A8: i in dom ((f ^ g) - (h ^ k)) by Th8;
percases ( i in dom f or not i in dom f ) ;
supposeA9: i in dom f ; ::_thesis: (sqr ((f ^ g) - (h ^ k))) . i = ((sqr (f - h)) ^ (sqr (g - k))) . i
then A10: i in dom (f - h) by A1, Th7;
then A11: i in dom (sqr (f - h)) by Th8;
A12: i in dom h by A1, A9, FINSEQ_3:29;
thus (sqr ((f ^ g) - (h ^ k))) . i = (((f ^ g) - (h ^ k)) . i) ^2 by VALUED_1:11
.= (((f ^ g) . i) - ((h ^ k) . i)) ^2 by A8, VALUED_1:13
.= ((f . i) - ((h ^ k) . i)) ^2 by A9, FINSEQ_1:def_7
.= ((f . i) - (h . i)) ^2 by A12, FINSEQ_1:def_7
.= ((f - h) . i) ^2 by A10, VALUED_1:13
.= (sqr (f - h)) . i by VALUED_1:11
.= ((sqr (f - h)) ^ (sqr (g - k))) . i by A11, FINSEQ_1:def_7 ; ::_thesis: verum
end;
suppose not i in dom f ; ::_thesis: (sqr ((f ^ g) - (h ^ k))) . i = ((sqr (f - h)) ^ (sqr (g - k))) . i
then A13: len f < i by A6, FINSEQ_3:25;
then reconsider j = i - (len f) as Element of NAT by INT_1:5;
A14: len (f - h) < i by A1, A13, Th7;
then A15: len (sqr (f - h)) < i by Th8;
 i <= len ((f ^ g) - (h ^ k)) by A7, Th8;
then A16: i <= len (f ^ g) by A1, A2, A3, A4, Th7;
then  i <= (len (f - h)) + (len g) by A1, A3, Th7;
then  i <= (len (f - h)) + (len (g - k)) by A2, Th7;
then  i - (len (f - h)) in dom (g - k) by A14, Th4;
then A17: j in dom (g - k) by A1, Th7;
 len f = len (f - h) by A1, Th7;
then A18: j = i - (len (sqr (f - h))) by Th8;
thus (sqr ((f ^ g) - (h ^ k))) . i = (((f ^ g) - (h ^ k)) . i) ^2 by VALUED_1:11
.= (((f ^ g) . i) - ((h ^ k) . i)) ^2 by A8, VALUED_1:13
.= ((g . j) - ((h ^ k) . i)) ^2 by A13, A16, FINSEQ_1:24
.= ((g . j) - (k . j)) ^2 by A1, A2, A3, A4, A13, A16, FINSEQ_1:24
.= ((g - k) . j) ^2 by A17, VALUED_1:13
.= (sqr (g - k)) . j by VALUED_1:11
.= ((sqr (f - h)) ^ (sqr (g - k))) . i by A5, A7, A15, A18, FINSEQ_1:24 ; ::_thesis: verum
end;
end;
end;
hence  sqr ((f ^ g) - (h ^ k)) = (sqr (f - h)) ^ (sqr (g - k)) by A5, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th15: :: TOPREAL7:15
for f, h, g, k being FinSequence of REAL st len f = len h & len g = len k holds
abs ((f ^ g) - (h ^ k)) = (abs (f - h)) ^ (abs (g - k))
proof
let f, h, g, k be FinSequence of REAL ; ::_thesis: ( len f = len h & len g = len k implies abs ((f ^ g) - (h ^ k)) = (abs (f - h)) ^ (abs (g - k)) )
assume that
A1: len f = len h and
A2: len g = len k ; ::_thesis: abs ((f ^ g) - (h ^ k)) = (abs (f - h)) ^ (abs (g - k))
A3: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
A4: len (h ^ k) = (len h) + (len k) by FINSEQ_1:22;
A5: len (abs ((f ^ g) - (h ^ k))) = len ((f ^ g) - (h ^ k)) by Th9
.= len (f ^ g) by A1, A2, A3, A4, Th7
.= (len (f - h)) + (len g) by A1, A3, Th7
.= (len (f - h)) + (len (g - k)) by A2, Th7
.= (len (abs (f - h))) + (len (g - k)) by Th9
.= (len (abs (f - h))) + (len (abs (g - k))) by Th9
.= len ((abs (f - h)) ^ (abs (g - k))) by FINSEQ_1:22 ;
 for i being Nat st 1 <= i & i <= len (abs ((f ^ g) - (h ^ k))) holds
(abs ((f ^ g) - (h ^ k))) . i = ((abs (f - h)) ^ (abs (g - k))) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (abs ((f ^ g) - (h ^ k))) implies (abs ((f ^ g) - (h ^ k))) . i = ((abs (f - h)) ^ (abs (g - k))) . i )
assume that
A6: 1 <= i and
A7: i <= len (abs ((f ^ g) - (h ^ k))) ; ::_thesis: (abs ((f ^ g) - (h ^ k))) . i = ((abs (f - h)) ^ (abs (g - k))) . i
A8: i in dom (abs ((f ^ g) - (h ^ k))) by A6, A7, FINSEQ_3:25;
then A9: i in dom ((f ^ g) - (h ^ k)) by Th9;
percases ( i in dom f or not i in dom f ) ;
supposeA10: i in dom f ; ::_thesis: (abs ((f ^ g) - (h ^ k))) . i = ((abs (f - h)) ^ (abs (g - k))) . i
reconsider i1 = i as Element of NAT by ORDINAL1:def_12;
A11: i in dom h by A1, A10, FINSEQ_3:29;
A12: i in dom (f - h) by A1, A10, Th7;
then A13: i in dom (abs (f - h)) by Th9;
thus (abs ((f ^ g) - (h ^ k))) . i = abs (((f ^ g) - (h ^ k)) . i1) by A8, TOPREAL6:12
.= abs (((f ^ g) . i) - ((h ^ k) . i)) by A9, VALUED_1:13
.= abs ((f . i) - ((h ^ k) . i)) by A10, FINSEQ_1:def_7
.= abs ((f . i) - (h . i)) by A11, FINSEQ_1:def_7
.= abs ((f - h) . i1) by A12, VALUED_1:13
.= (abs (f - h)) . i1 by A13, TOPREAL6:12
.= ((abs (f - h)) ^ (abs (g - k))) . i by A13, FINSEQ_1:def_7 ; ::_thesis: verum
end;
supposeA14: not i in dom f ; ::_thesis: (abs ((f ^ g) - (h ^ k))) . i = ((abs (f - h)) ^ (abs (g - k))) . i
reconsider i1 = i as Element of NAT by ORDINAL1:def_12;
A15: len f < i by A6, A14, FINSEQ_3:25;
then reconsider j = i - (len f) as Element of NAT by INT_1:5;
A16: len (f - h) < i by A1, A15, Th7;
then A17: len (abs (f - h)) < i by Th9;
 i <= len ((f ^ g) - (h ^ k)) by A7, Th9;
then A18: i <= len (f ^ g) by A1, A2, A3, A4, Th7;
then  i <= (len (f - h)) + (len g) by A1, A3, Th7;
then  i <= (len (f - h)) + (len (g - k)) by A2, Th7;
then  i - (len (f - h)) in dom (g - k) by A16, Th4;
then A19: j in dom (g - k) by A1, Th7;
then A20: j in dom (abs (g - k)) by Th9;
 len f = len (f - h) by A1, Th7;
then A21: j = i - (len (abs (f - h))) by Th9;
thus (abs ((f ^ g) - (h ^ k))) . i = abs (((f ^ g) - (h ^ k)) . i1) by A8, TOPREAL6:12
.= abs (((f ^ g) . i) - ((h ^ k) . i)) by A9, VALUED_1:13
.= abs ((g . j) - ((h ^ k) . i)) by A15, A18, FINSEQ_1:24
.= abs ((g . j) - (k . j)) by A1, A2, A3, A4, A15, A18, FINSEQ_1:24
.= abs ((g - k) . j) by A19, VALUED_1:13
.= (abs (g - k)) . j by A20, TOPREAL6:12
.= ((abs (f - h)) ^ (abs (g - k))) . i by A5, A7, A17, A21, FINSEQ_1:24 ; ::_thesis: verum
end;
end;
end;
hence  abs ((f ^ g) - (h ^ k)) = (abs (f - h)) ^ (abs (g - k)) by A5, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th16: :: TOPREAL7:16
for n being Element of NAT
for f being FinSequence of REAL st len f = n holds
f in the carrier of (Euclid n) by TOPREAL3:45;

theorem :: TOPREAL7:17
for n being Element of NAT
for f being FinSequence of REAL st len f = n holds
f in the carrier of (TOP-REAL n) by TOPREAL3:46;

definition
let M, N be non empty MetrStruct ;
func max-Prod2 (M,N) ->  strict MetrStruct  means :Def1: :: TOPREAL7:def 1
( the carrier of it = [: the carrier of M, the carrier of N:] & ( for x, y being Point of it ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of it . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) );
existence
 ex b1 being strict MetrStruct st
( the carrier of b1 = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b1 ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of b1 . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) )
proof
defpred S1[ set , set , set ] means  ex x1, y1 being Point of M ex x2, y2 being Point of N st
( $1 = [x1,x2] & $2 = [y1,y2] & $3 = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) );
set C = [: the carrier of M, the carrier of N:];
A1: for x, y being Element of [: the carrier of M, the carrier of N:] ex u being Element of REAL st S1[x,y,u]
proof
let x, y be Element of [: the carrier of M, the carrier of N:]; ::_thesis: ex u being Element of REAL st S1[x,y,u]
set x1 = x `1 ;
set x2 = x `2 ;
set y1 = y `1 ;
set y2 = y `2 ;
take  max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) ; ::_thesis: S1[x,y, max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2))))]
take  x `1 ; ::_thesis: ex y1 being Point of M ex x2, y2 being Point of N st
( x = [(x `1),x2] & y = [y1,y2] & max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) = max (( the distance of M . ((x `1),y1)),( the distance of N . (x2,y2))) )
take  y `1 ; ::_thesis: ex x2, y2 being Point of N st
( x = [(x `1),x2] & y = [(y `1),y2] & max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) = max (( the distance of M . ((x `1),(y `1))),( the distance of N . (x2,y2))) )
take  x `2 ; ::_thesis: ex y2 being Point of N st
( x = [(x `1),(x `2)] & y = [(y `1),y2] & max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) = max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),y2))) )
take  y `2 ; ::_thesis: ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] & max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) = max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) )
thus  ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] & max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) = max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) ) by MCART_1:21; ::_thesis: verum
end;
consider f being Function of [:[: the carrier of M, the carrier of N:],[: the carrier of M, the carrier of N:]:],REAL such that
A2: for x, y being Element of [: the carrier of M, the carrier of N:] holds S1[x,y,f . (x,y)] from BINOP_1:sch_3(A1);
take E = MetrStruct(# [: the carrier of M, the carrier of N:],f #); ::_thesis: ( the carrier of E = [: the carrier of M, the carrier of N:] & ( for x, y being Point of E ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) )
thus  the carrier of E = [: the carrier of M, the carrier of N:] ; ::_thesis: for x, y being Point of E ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )
let x, y be Point of E; ::_thesis: ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A3: ( x = [x1,x2] & y = [y1,y2] & f . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) by A2;
take  x1 ; ::_thesis: ex y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )
take  y1 ; ::_thesis: ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )
take  x2 ; ::_thesis: ex y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )
take  y2 ; ::_thesis: ( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )
thus  ( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) by A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict MetrStruct st the carrier of b1 = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b1 ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of b1 . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) & the carrier of b2 = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b2 ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of b2 . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) holds
b1 = b2
proof
let A, B be strict MetrStruct ; ::_thesis: ( the carrier of A = [: the carrier of M, the carrier of N:] & ( for x, y being Point of A ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of A . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) & the carrier of B = [: the carrier of M, the carrier of N:] & ( for x, y being Point of B ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of B . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) implies A = B )
assume that
A4: the carrier of A = [: the carrier of M, the carrier of N:] and
A5: for x, y being Point of A ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of A . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) and
A6: the carrier of B = [: the carrier of M, the carrier of N:] and
A7: for x, y being Point of B ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of B . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ; ::_thesis: A = B
set f = the distance of A;
set g = the distance of B;
 for a, b being set st a in the carrier of A & b in the carrier of A holds
the distance of A . (a,b) = the distance of B . (a,b)
proof
let a, b be set ; ::_thesis: ( a in the carrier of A & b in the carrier of A implies the distance of A . (a,b) = the distance of B . (a,b) )
assume A8: ( a in the carrier of A & b in the carrier of A ) ; ::_thesis: the distance of A . (a,b) = the distance of B . (a,b)
then consider x1, y1 being Point of M, x2, y2 being Point of N such that
A9: a = [x1,x2] and
A10: b = [y1,y2] and
A11: the distance of A . (a,b) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by A5;
consider m1, n1 being Point of M, m2, n2 being Point of N such that
A12: a = [m1,m2] and
A13: b = [n1,n2] and
A14: the distance of B . (a,b) = max (( the distance of M . (m1,n1)),( the distance of N . (m2,n2))) by A4, A6, A7, A8;
A15: y1 = n1 by A10, A13, XTUPLE_0:1;
 ( x1 = m1 & x2 = m2 ) by A9, A12, XTUPLE_0:1;
hence  the distance of A . (a,b) = the distance of B . (a,b) by A10, A11, A13, A14, A15, XTUPLE_0:1; ::_thesis: verum
end;
hence  A = B by A4, A6, BINOP_1:1; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines max-Prod2 TOPREAL7:def_1_:_
 for M, N being non empty MetrStruct
for b3 being strict MetrStruct holds
( b3 = max-Prod2 (M,N) iff ( the carrier of b3 = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b3 ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of b3 . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) ) );

registration
let M, N be non empty MetrStruct ;
cluster max-Prod2 (M,N) ->  non empty strict ;
coherence
 not max-Prod2 (M,N) is empty
proof
 the carrier of (max-Prod2 (M,N)) = [: the carrier of M, the carrier of N:] by Def1;
hence  not the carrier of (max-Prod2 (M,N)) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

definition
let M, N be non empty MetrStruct ;
let x be Point of M;
let y be Point of N;
:: original: [
redefine func[x,y] ->  Element of (max-Prod2 (M,N));
coherence
 [x,y] is Element of (max-Prod2 (M,N))
proof
 [x,y] is Element of (max-Prod2 (M,N)) by Def1;
hence  [x,y] is Element of (max-Prod2 (M,N)) ; ::_thesis: verum
end;
end;

definition
let M, N be non empty MetrStruct ;
let x be Point of (max-Prod2 (M,N));
:: original: `1
redefine funcx `1  ->  Element of M;
coherence
 x `1 is Element of M
proof
 the carrier of (max-Prod2 (M,N)) = [: the carrier of M, the carrier of N:] by Def1;
hence  x `1 is Element of M by MCART_1:10; ::_thesis: verum
end;
:: original: `2
redefine funcx `2  ->  Element of N;
coherence
 x `2 is Element of N
proof
 the carrier of (max-Prod2 (M,N)) = [: the carrier of M, the carrier of N:] by Def1;
hence  x `2 is Element of N by MCART_1:10; ::_thesis: verum
end;
end;

theorem Th18: :: TOPREAL7:18
for M, N being non empty MetrStruct
for m1, m2 being Point of M
for n1, n2 being Point of N holds dist ([m1,n1],[m2,n2]) = max ((dist (m1,m2)),(dist (n1,n2)))
proof
let M, N be non empty MetrStruct ; ::_thesis: for m1, m2 being Point of M
for n1, n2 being Point of N holds dist ([m1,n1],[m2,n2]) = max ((dist (m1,m2)),(dist (n1,n2)))
let m1, m2 be Point of M; ::_thesis: for n1, n2 being Point of N holds dist ([m1,n1],[m2,n2]) = max ((dist (m1,m2)),(dist (n1,n2)))
let n1, n2 be Point of N; ::_thesis: dist ([m1,n1],[m2,n2]) = max ((dist (m1,m2)),(dist (n1,n2)))
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A1: [m1,n1] = [x1,x2] and
A2: [m2,n2] = [y1,y2] and
A3: the distance of (max-Prod2 (M,N)) . ([m1,n1],[m2,n2]) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1;
A4: m2 = y1 by A2, XTUPLE_0:1;
 ( m1 = x1 & n1 = x2 ) by A1, XTUPLE_0:1;
hence  dist ([m1,n1],[m2,n2]) = max ((dist (m1,m2)),(dist (n1,n2))) by A2, A3, A4, XTUPLE_0:1; ::_thesis: verum
end;

theorem :: TOPREAL7:19
for M, N being non empty MetrStruct
for m, n being Point of (max-Prod2 (M,N)) holds dist (m,n) = max ((dist ((m `1),(n `1))),(dist ((m `2),(n `2))))
proof
let M, N be non empty MetrStruct ; ::_thesis: for m, n being Point of (max-Prod2 (M,N)) holds dist (m,n) = max ((dist ((m `1),(n `1))),(dist ((m `2),(n `2))))
let m, n be Point of (max-Prod2 (M,N)); ::_thesis: dist (m,n) = max ((dist ((m `1),(n `1))),(dist ((m `2),(n `2))))
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A1: m = [x1,x2] and
A2: n = [y1,y2] and
A3: the distance of (max-Prod2 (M,N)) . (m,n) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1;
A4: m `2 = x2 by A1, MCART_1:7;
 ( m `1 = x1 & n `1 = y1 ) by A1, A2, MCART_1:7;
hence  dist (m,n) = max ((dist ((m `1),(n `1))),(dist ((m `2),(n `2)))) by A2, A3, A4, MCART_1:7; ::_thesis: verum
end;

theorem Th20: :: TOPREAL7:20
for M, N being non empty Reflexive MetrStruct holds max-Prod2 (M,N) is Reflexive
proof
let M, N be non empty Reflexive MetrStruct ; ::_thesis: max-Prod2 (M,N) is Reflexive
let a be Element of (max-Prod2 (M,N)); :: according to METRIC_1:def_2,METRIC_1:def_6 ::_thesis: the distance of (max-Prod2 (M,N)) . (a,a) = 0
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A1: ( a = [x1,x2] & a = [y1,y2] ) and
A2: the distance of (max-Prod2 (M,N)) . (a,a) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1;
 the distance of M is Reflexive by METRIC_1:def_6;
then A3: the distance of M . (x1,x1) = 0 by METRIC_1:def_2;
 the distance of N is Reflexive by METRIC_1:def_6;
then A4: the distance of N . (x2,x2) = 0 by METRIC_1:def_2;
 ( x1 = y1 & x2 = y2 ) by A1, XTUPLE_0:1;
hence  the distance of (max-Prod2 (M,N)) . (a,a) = 0 by A2, A3, A4; ::_thesis: verum
end;

registration
let M, N be non empty Reflexive MetrStruct ;
cluster max-Prod2 (M,N) ->  strict Reflexive ;
coherence
 max-Prod2 (M,N) is Reflexive by Th20;
end;

Lm1:  for M, N being non empty MetrSpace holds max-Prod2 (M,N) is discerning
proof
let M, N be non empty MetrSpace; ::_thesis: max-Prod2 (M,N) is discerning
let a, b be Element of (max-Prod2 (M,N)); :: according to METRIC_1:def_3,METRIC_1:def_7 ::_thesis: ( not the distance of (max-Prod2 (M,N)) . (a,b) = 0 or a = b )
assume A1: the distance of (max-Prod2 (M,N)) . (a,b) = 0 ; ::_thesis: a = b
A2: the distance of M is discerning by METRIC_1:def_7;
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A3: ( a = [x1,x2] & b = [y1,y2] ) and
A4: the distance of (max-Prod2 (M,N)) . (a,b) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1;
 0 <= dist (x1,y1) by METRIC_1:5;
then  the distance of M . (x1,y1) = 0 by A1, A4, XXREAL_0:49;
then A5: ( the distance of N is discerning & x1 = y1 ) by A2, METRIC_1:def_3, METRIC_1:def_7;
 0 <= dist (x2,y2) by METRIC_1:5;
then  the distance of N . (x2,y2) = 0 by A1, A4, XXREAL_0:49;
hence  a = b by A3, A5, METRIC_1:def_3; ::_thesis: verum
end;

theorem Th21: :: TOPREAL7:21
for M, N being non empty symmetric MetrStruct holds max-Prod2 (M,N) is symmetric
proof
let M, N be non empty symmetric MetrStruct ; ::_thesis: max-Prod2 (M,N) is symmetric
let a, b be Element of (max-Prod2 (M,N)); :: according to METRIC_1:def_4,METRIC_1:def_8 ::_thesis: the distance of (max-Prod2 (M,N)) . (a,b) = the distance of (max-Prod2 (M,N)) . (b,a)
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A1: a = [x1,x2] and
A2: b = [y1,y2] and
A3: the distance of (max-Prod2 (M,N)) . (a,b) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1;
consider m1, n1 being Point of M, m2, n2 being Point of N such that
A4: b = [m1,m2] and
A5: a = [n1,n2] and
A6: the distance of (max-Prod2 (M,N)) . (b,a) = max (( the distance of M . (m1,n1)),( the distance of N . (m2,n2))) by Def1;
A7: x1 = n1 by A1, A5, XTUPLE_0:1;
 the distance of N is symmetric by METRIC_1:def_8;
then A8: the distance of N . (x2,y2) = the distance of N . (y2,x2) by METRIC_1:def_4;
 the distance of M is symmetric by METRIC_1:def_8;
then A9: the distance of M . (x1,y1) = the distance of M . (y1,x1) by METRIC_1:def_4;
 ( y1 = m1 & y2 = m2 ) by A2, A4, XTUPLE_0:1;
hence  the distance of (max-Prod2 (M,N)) . (a,b) = the distance of (max-Prod2 (M,N)) . (b,a) by A1, A3, A5, A6, A9, A8, A7, XTUPLE_0:1; ::_thesis: verum
end;

registration
let M, N be non empty symmetric MetrStruct ;
cluster max-Prod2 (M,N) ->  strict symmetric ;
coherence
 max-Prod2 (M,N) is symmetric by Th21;
end;

theorem Th22: :: TOPREAL7:22
for M, N being non empty triangle MetrStruct holds max-Prod2 (M,N) is triangle
proof
let M, N be non empty triangle MetrStruct ; ::_thesis: max-Prod2 (M,N) is triangle
let a, b, c be Element of (max-Prod2 (M,N)); :: according to METRIC_1:def_5,METRIC_1:def_9 ::_thesis: the distance of (max-Prod2 (M,N)) . (a,c) <= ( the distance of (max-Prod2 (M,N)) . (a,b)) + ( the distance of (max-Prod2 (M,N)) . (b,c))
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A1: a = [x1,x2] and
A2: b = [y1,y2] and
A3: the distance of (max-Prod2 (M,N)) . (a,b) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1;
consider m1, n1 being Point of M, m2, n2 being Point of N such that
A4: b = [m1,m2] and
A5: c = [n1,n2] and
A6: the distance of (max-Prod2 (M,N)) . (b,c) = max (( the distance of M . (m1,n1)),( the distance of N . (m2,n2))) by Def1;
A7: ( y1 = m1 & y2 = m2 ) by A2, A4, XTUPLE_0:1;
consider p1, q1 being Point of M, p2, q2 being Point of N such that
A8: a = [p1,p2] and
A9: c = [q1,q2] and
A10: the distance of (max-Prod2 (M,N)) . (a,c) = max (( the distance of M . (p1,q1)),( the distance of N . (p2,q2))) by Def1;
A11: ( q1 = n1 & q2 = n2 ) by A5, A9, XTUPLE_0:1;
 the distance of N is triangle by METRIC_1:def_9;
then A12: the distance of N . (p2,q2) <= ( the distance of N . (p2,y2)) + ( the distance of N . (y2,q2)) by METRIC_1:def_5;
 the distance of M is triangle by METRIC_1:def_9;
then A13: the distance of M . (p1,q1) <= ( the distance of M . (p1,y1)) + ( the distance of M . (y1,q1)) by METRIC_1:def_5;
 ( x1 = p1 & x2 = p2 ) by A1, A8, XTUPLE_0:1;
hence  the distance of (max-Prod2 (M,N)) . (a,c) <= ( the distance of (max-Prod2 (M,N)) . (a,b)) + ( the distance of (max-Prod2 (M,N)) . (b,c)) by A3, A6, A10, A13, A12, A7, A11, Th2; ::_thesis: verum
end;

registration
let M, N be non empty triangle MetrStruct ;
cluster max-Prod2 (M,N) ->  strict triangle ;
coherence
 max-Prod2 (M,N) is triangle by Th22;
end;

registration
let M, N be non empty MetrSpace;
cluster max-Prod2 (M,N) ->  strict discerning ;
coherence
 max-Prod2 (M,N) is discerning by Lm1;
end;

theorem Th23: :: TOPREAL7:23
for M, N being non empty MetrSpace holds [:(TopSpaceMetr M),(TopSpaceMetr N):] = TopSpaceMetr (max-Prod2 (M,N))
proof
let M, N be non empty MetrSpace; ::_thesis: [:(TopSpaceMetr M),(TopSpaceMetr N):] = TopSpaceMetr (max-Prod2 (M,N))
set S = TopSpaceMetr M;
set T = TopSpaceMetr N;
A1: TopSpaceMetr (max-Prod2 (M,N)) = TopStruct(# the carrier of (max-Prod2 (M,N)),(Family_open_set (max-Prod2 (M,N))) #) by PCOMPS_1:def_5;
A2: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
A3: TopSpaceMetr N = TopStruct(# the carrier of N,(Family_open_set N) #) by PCOMPS_1:def_5;
A4: the carrier of [:(TopSpaceMetr M),(TopSpaceMetr N):] = [: the carrier of (TopSpaceMetr M), the carrier of (TopSpaceMetr N):] by BORSUK_1:def_2
.= the carrier of (TopSpaceMetr (max-Prod2 (M,N))) by A1, A2, A3, Def1 ;
A5: the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] =  {  (union A) where A is Subset-Family of [:(TopSpaceMetr M),(TopSpaceMetr N):] : A c=  {  [:X1,X2:] where X1 is Subset of (TopSpaceMetr M), X2 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & X2 in the topology of (TopSpaceMetr N) )  }   }  by BORSUK_1:def_2;
 the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] = the topology of (TopSpaceMetr (max-Prod2 (M,N)))
proof
thus  the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] c= the topology of (TopSpaceMetr (max-Prod2 (M,N))) :: according to XBOOLE_0:def_10 ::_thesis: the topology of (TopSpaceMetr (max-Prod2 (M,N))) c= the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):]
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] or X in the topology of (TopSpaceMetr (max-Prod2 (M,N))) )
assume A6: X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] ; ::_thesis: X in the topology of (TopSpaceMetr (max-Prod2 (M,N)))
then consider A being Subset-Family of [:(TopSpaceMetr M),(TopSpaceMetr N):] such that
A7: X = union A and
A8: A c=  {  [:X1,X2:] where X1 is Subset of (TopSpaceMetr M), X2 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & X2 in the topology of (TopSpaceMetr N) )  }  by A5;
 for x being Point of (max-Prod2 (M,N)) st x in X holds
ex r being Real st
( r > 0 & Ball (x,r) c= X )
proof
let x be Point of (max-Prod2 (M,N)); ::_thesis: ( x in X implies ex r being Real st
( r > 0 & Ball (x,r) c= X ) )
assume  x in X ; ::_thesis: ex r being Real st
( r > 0 & Ball (x,r) c= X )
then consider Z being set  such that
A9: x in Z and
A10: Z in A by A7, TARSKI:def_4;
 Z in  {  [:X1,X2:] where X1 is Subset of (TopSpaceMetr M), X2 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & X2 in the topology of (TopSpaceMetr N) )  }  by A8, A10;
then consider X1 being Subset of (TopSpaceMetr M), X2 being Subset of (TopSpaceMetr N) such that
A11: Z = [:X1,X2:] and
A12: X1 in the topology of (TopSpaceMetr M) and
A13: X2 in the topology of (TopSpaceMetr N) ;
consider z1, z2 being set  such that
A14: z1 in X1 and
A15: z2 in X2 and
A16: x = [z1,z2] by A9, A11, ZFMISC_1:def_2;
reconsider z2 = z2 as Point of N by A3, A15;
consider r2 being Real such that
A17: r2 > 0 and
A18: Ball (z2,r2) c= X2 by A3, A13, A15, PCOMPS_1:def_4;
reconsider z1 = z1 as Point of M by A2, A14;
consider r1 being Real such that
A19: r1 > 0 and
A20: Ball (z1,r1) c= X1 by A2, A12, A14, PCOMPS_1:def_4;
take r = min (r1,r2); ::_thesis: ( r > 0 & Ball (x,r) c= X )
thus  r > 0 by A19, A17, XXREAL_0:15; ::_thesis: Ball (x,r) c= X
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (x,r) or b in X )
assume A21: b in Ball (x,r) ; ::_thesis: b in X
then reconsider bb = b as Point of (max-Prod2 (M,N)) ;
A22: dist (bb,x) < r by A21, METRIC_1:11;
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A23: bb = [x1,x2] and
A24: x = [y1,y2] and
A25: the distance of (max-Prod2 (M,N)) . (bb,x) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1;
 z2 = y2 by A16, A24, XTUPLE_0:1;
then  the distance of N . (x2,z2) <= max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by XXREAL_0:25;
then  ( min (r1,r2) <= r2 & the distance of N . (x2,z2) < r ) by A25, A22, XXREAL_0:2, XXREAL_0:17;
then  dist (x2,z2) < r2 by XXREAL_0:2;
then A26: x2 in Ball (z2,r2) by METRIC_1:11;
 z1 = y1 by A16, A24, XTUPLE_0:1;
then  the distance of M . (x1,z1) <= max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by XXREAL_0:25;
then  ( min (r1,r2) <= r1 & the distance of M . (x1,z1) < r ) by A25, A22, XXREAL_0:2, XXREAL_0:17;
then  dist (x1,z1) < r1 by XXREAL_0:2;
then  x1 in Ball (z1,r1) by METRIC_1:11;
then  b in [:X1,X2:] by A20, A18, A23, A26, ZFMISC_1:87;
hence  b in X by A7, A10, A11, TARSKI:def_4; ::_thesis: verum
end;
hence  X in the topology of (TopSpaceMetr (max-Prod2 (M,N))) by A1, A4, A6, PCOMPS_1:def_4; ::_thesis: verum
end;
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in the topology of (TopSpaceMetr (max-Prod2 (M,N))) or X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] )
assume A27: X in the topology of (TopSpaceMetr (max-Prod2 (M,N))) ; ::_thesis: X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):]
then reconsider Y = X as Subset of [:(TopSpaceMetr M),(TopSpaceMetr N):] by A4;
A28: Base-Appr Y =  {  [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( [:X1,Y1:] c= Y & X1 is open & Y1 is open )  }  by BORSUK_1:def_3;
A29: union (Base-Appr Y) = Y
proof
thus  union (Base-Appr Y) c= Y by BORSUK_1:12; :: according to XBOOLE_0:def_10 ::_thesis: Y c= union (Base-Appr Y)
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in Y or u in union (Base-Appr Y) )
assume A30: u in Y ; ::_thesis: u in union (Base-Appr Y)
then reconsider uu = u as Point of (max-Prod2 (M,N)) by A1, A4;
consider r being Real such that
A31: r > 0 and
A32: Ball (uu,r) c= Y by A1, A27, A30, PCOMPS_1:def_4;
 uu in the carrier of (max-Prod2 (M,N)) ;
then  uu in [: the carrier of M, the carrier of N:] by Def1;
then consider u1, u2 being set  such that
A33: u1 in the carrier of M and
A34: u2 in the carrier of N and
A35: u = [u1,u2] by ZFMISC_1:def_2;
reconsider u2 = u2 as Point of N by A34;
reconsider u1 = u1 as Point of M by A33;
reconsider B2 = Ball (u2,r) as Subset of (TopSpaceMetr N) by A3;
reconsider B1 = Ball (u1,r) as Subset of (TopSpaceMetr M) by A2;
 ( u1 in Ball (u1,r) & u2 in Ball (u2,r) ) by A31, TBSP_1:11;
then A36: u in [:B1,B2:] by A35, ZFMISC_1:87;
A37: [:B1,B2:] c= Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:B1,B2:] or x in Y )
assume  x in [:B1,B2:] ; ::_thesis: x in Y
then consider x1, x2 being set  such that
A38: x1 in B1 and
A39: x2 in B2 and
A40: x = [x1,x2] by ZFMISC_1:def_2;
reconsider x2 = x2 as Point of N by A39;
reconsider x1 = x1 as Point of M by A38;
consider p1, p2 being Point of M, q1, q2 being Point of N such that
A41: ( uu = [p1,q1] & [x1,x2] = [p2,q2] ) and
A42: the distance of (max-Prod2 (M,N)) . (uu,[x1,x2]) = max (( the distance of M . (p1,p2)),( the distance of N . (q1,q2))) by Def1;
 ( u2 = q1 & x2 = q2 ) by A35, A41, XTUPLE_0:1;
then A43: dist (q1,q2) < r by A39, METRIC_1:11;
 ( u1 = p1 & x1 = p2 ) by A35, A41, XTUPLE_0:1;
then  dist (p1,p2) < r by A38, METRIC_1:11;
then  dist (uu,[x1,x2]) < r by A42, A43, XXREAL_0:16;
then  x in Ball (uu,r) by A40, METRIC_1:11;
hence  x in Y by A32; ::_thesis: verum
end;
 ( B1 is open & B2 is open ) by TOPMETR:14;
then  [:B1,B2:] in Base-Appr Y by A28, A37;
hence  u in union (Base-Appr Y) by A36, TARSKI:def_4; ::_thesis: verum
end;
 Base-Appr Y c=  {  [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) )  }
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in Base-Appr Y or A in  {  [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) )  }  )
assume  A in Base-Appr Y ; ::_thesis: A in  {  [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) )  }
then consider X1 being Subset of (TopSpaceMetr M), Y1 being Subset of (TopSpaceMetr N) such that
A44: A = [:X1,Y1:] and
 [:X1,Y1:] c= Y and
A45: ( X1 is open & Y1 is open ) by A28;
 ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) ) by A45, PRE_TOPC:def_2;
hence  A in  {  [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) )  }  by A44; ::_thesis: verum
end;
hence  X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] by A5, A29; ::_thesis: verum
end;
hence  [:(TopSpaceMetr M),(TopSpaceMetr N):] = TopSpaceMetr (max-Prod2 (M,N)) by A4; ::_thesis: verum
end;

theorem :: TOPREAL7:24
for M, N being non empty MetrSpace st the carrier of M = the carrier of N & ( for m being Point of M
for n being Point of N
for r being Real st r > 0 & m = n holds
ex r1 being Real st
( r1 > 0 & Ball (n,r1) c= Ball (m,r) ) ) & ( for m being Point of M
for n being Point of N
for r being Real st r > 0 & m = n holds
ex r1 being Real st
( r1 > 0 & Ball (m,r1) c= Ball (n,r) ) ) holds
TopSpaceMetr M = TopSpaceMetr N
proof
let M, N be non empty MetrSpace; ::_thesis: ( the carrier of M = the carrier of N & ( for m being Point of M
for n being Point of N
for r being Real st r > 0 & m = n holds
ex r1 being Real st
( r1 > 0 & Ball (n,r1) c= Ball (m,r) ) ) & ( for m being Point of M
for n being Point of N
for r being Real st r > 0 & m = n holds
ex r1 being Real st
( r1 > 0 & Ball (m,r1) c= Ball (n,r) ) ) implies TopSpaceMetr M = TopSpaceMetr N )
assume that
A1: the carrier of M = the carrier of N and
A2: for m being Point of M
for n being Point of N
for r being Real st r > 0 & m = n holds
ex r1 being Real st
( r1 > 0 & Ball (n,r1) c= Ball (m,r) ) and
A3: for m being Point of M
for n being Point of N
for r being Real st r > 0 & m = n holds
ex r1 being Real st
( r1 > 0 & Ball (m,r1) c= Ball (n,r) ) ; ::_thesis: TopSpaceMetr M = TopSpaceMetr N
A4: Family_open_set M = Family_open_set N
proof
thus  Family_open_set M c= Family_open_set N :: according to XBOOLE_0:def_10 ::_thesis: Family_open_set N c= Family_open_set M
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in Family_open_set M or X in Family_open_set N )
assume A5: X in Family_open_set M ; ::_thesis: X in Family_open_set N
 for n being Point of N st n in X holds
ex r being Real st
( r > 0 & Ball (n,r) c= X )
proof
let n be Point of N; ::_thesis: ( n in X implies ex r being Real st
( r > 0 & Ball (n,r) c= X ) )
assume A6: n in X ; ::_thesis: ex r being Real st
( r > 0 & Ball (n,r) c= X )
reconsider m = n as Point of M by A1;
consider r being Real such that
A7: r > 0 and
A8: Ball (m,r) c= X by A5, A6, PCOMPS_1:def_4;
consider r1 being Real such that
A9: ( r1 > 0 & Ball (n,r1) c= Ball (m,r) ) by A2, A7;
take  r1 ; ::_thesis: ( r1 > 0 & Ball (n,r1) c= X )
thus  ( r1 > 0 & Ball (n,r1) c= X ) by A8, A9, XBOOLE_1:1; ::_thesis: verum
end;
hence  X in Family_open_set N by A1, A5, PCOMPS_1:def_4; ::_thesis: verum
end;
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in Family_open_set N or X in Family_open_set M )
assume A10: X in Family_open_set N ; ::_thesis: X in Family_open_set M
 for m being Point of M st m in X holds
ex r being Real st
( r > 0 & Ball (m,r) c= X )
proof
let m be Point of M; ::_thesis: ( m in X implies ex r being Real st
( r > 0 & Ball (m,r) c= X ) )
assume A11: m in X ; ::_thesis: ex r being Real st
( r > 0 & Ball (m,r) c= X )
reconsider n = m as Point of N by A1;
consider r being Real such that
A12: r > 0 and
A13: Ball (n,r) c= X by A10, A11, PCOMPS_1:def_4;
consider r1 being Real such that
A14: ( r1 > 0 & Ball (m,r1) c= Ball (n,r) ) by A3, A12;
take  r1 ; ::_thesis: ( r1 > 0 & Ball (m,r1) c= X )
thus  ( r1 > 0 & Ball (m,r1) c= X ) by A13, A14, XBOOLE_1:1; ::_thesis: verum
end;
hence  X in Family_open_set M by A1, A10, PCOMPS_1:def_4; ::_thesis: verum
end;
 TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
hence  TopSpaceMetr M = TopSpaceMetr N by A1, A4, PCOMPS_1:def_5; ::_thesis: verum
end;

Lm2:  for i, j being Element of NAT 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 ) )
proof
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 S1[ 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 S1[x,y,u]
proof
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 S1[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 S1[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: S1[x,y,u]
thus  S1[x,y,u] ; ::_thesis: verum
end;
consider f being Function of [: the carrier of (Euclid i), the carrier of (Euclid j):], the carrier of (Euclid (i + j)) such that
A3: for x being Element of the carrier of (Euclid i)
for y being Element of the carrier of (Euclid j) holds S1[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 ) )
proof
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 set ; :: 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;
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
f . (fi,fj) = fi ^ fj ) )
proof
let x1, x2 be set ; :: 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 set  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 set  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;
A27: for P being Subset of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) st P is open holds
(f ") " P is open
proof
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)))) by PRE_TOPC:def_2;
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
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 set  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 set ; :: 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 set  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, MCART_1:7;
 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, MCART_1:7;
 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;
 f .: P is Subset of (Euclid (i + j)) by TOPMETR:12;
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;
A56: for P being Subset of (TopSpaceMetr (Euclid (i + j))) st P is open holds
f " P is open
proof
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))) by PRE_TOPC:def_2;
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
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 set ; :: 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;
 f " P is Subset of (max-Prod2 ((Euclid i),(Euclid j))) by A5, TOPMETR:12;
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;
 [#] (TopSpaceMetr (Euclid (i + j))) <> {} ;
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;
 S1[Fi,Fj,f . (Fi,Fj)] by A3;
hence  f . (fi,fj) = fi ^ fj ; ::_thesis: verum
end;

theorem :: TOPREAL7:25
for i, j being Element of NAT holds [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], TopSpaceMetr (Euclid (i + j)) are_homeomorphic
proof
let i, j be Element of NAT ; ::_thesis: [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], TopSpaceMetr (Euclid (i + j)) are_homeomorphic
consider f being Function of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):],(TopSpaceMetr (Euclid (i + j))) such that
A1: f is being_homeomorphism and
 for fi, fj being FinSequence st [fi,fj] in dom f holds
f . (fi,fj) = fi ^ fj by Lm2;
take  f ; :: according to T_0TOPSP:def_1 ::_thesis: f is being_homeomorphism
thus  f is being_homeomorphism by A1; ::_thesis: verum
end;

theorem :: TOPREAL7:26
for i, j being Element of NAT 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 ) ) by Lm2;