:: Homeomorphism between [:TOP-REAL i,TOP-REAL j:] and TOP-REAL (i+j)
:: by Artur Korni{\l}owicz
::
:: Received February 21, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

theorem Th1: :: TOPREAL7:1
for a, b, c, d being Real holds max ((a + c),(b + d)) <= (max (a,b)) + (max (c,d))
proofend;

theorem Th2: :: TOPREAL7:2
for a, b, c, d, e, f being Real st a <= b + c &amp; d <= e + f holds
max (a,d) <= (max (b,e)) + (max (c,f))
proofend;

theorem :: TOPREAL7:3
for f, g being FinSequence holds dom g c= dom (f ^ g)
proofend;

theorem Th4: :: TOPREAL7:4
for i being Nat
for f, g being FinSequence st len f < i &amp; i <= (len f) + (len g) holds
i - (len f) in dom g
proofend;

theorem Th5: :: TOPREAL7:5
for f, g, h, k being FinSequence st f ^ g = h ^ k &amp; len f = len h &amp; len g = len k holds
( f = h &amp; g = k )
proofend;

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 &amp; dom (f + g) = dom f )
proofend;

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 &amp; dom (f - g) = dom f )
proofend;

theorem Th8: :: TOPREAL7:8
for f being FinSequence of REAL holds
( len f = len (sqr f) &amp; 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) &amp; dom f = dom (abs f) )
proofend;

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)
proofend;

theorem :: TOPREAL7:12
for f, h, g, k being FinSequence of REAL st len f = len h &amp; len g = len k holds
sqr ((f ^ g) + (h ^ k)) = (sqr (f + h)) ^ (sqr (g + k))
proofend;

theorem :: TOPREAL7:13
for f, h, g, k being FinSequence of REAL st len f = len h &amp; len g = len k holds
abs ((f ^ g) + (h ^ k)) = (abs (f + h)) ^ (abs (g + k))
proofend;

theorem :: TOPREAL7:14
for f, h, g, k being FinSequence of REAL st len f = len h &amp; len g = len k holds
sqr ((f ^ g) - (h ^ k)) = (sqr (f - h)) ^ (sqr (g - k))
proofend;

theorem Th15: :: TOPREAL7:15
for f, h, g, k being FinSequence of REAL st len f = len h &amp; len g = len k holds
abs ((f ^ g) - (h ^ k)) = (abs (f - h)) ^ (abs (g - k))
proofend;

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:] &amp; ( 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] &amp; y = [y1,y2] &amp; 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:] &amp; ( 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] &amp; y = [y1,y2] &amp; the distance of b1 . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) )
proofend;
uniqueness
 for b1, b2 being strict MetrStruct st the carrier of b1 = [: the carrier of M, the carrier of N:] &amp; ( 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] &amp; y = [y1,y2] &amp; the distance of b1 . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) &amp; the carrier of b2 = [: the carrier of M, the carrier of N:] &amp; ( 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] &amp; y = [y1,y2] &amp; the distance of b2 . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) holds
b1 = b2
proofend;
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:] &amp; ( 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] &amp; y = [y1,y2] &amp; 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
proofend;
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))
proofend;
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
proofend;
:: original:`2
redefine funcx `2  ->  Element of N;
coherence
 x `2 is Element of N
proofend;
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)))
proofend;

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))))
proofend;

theorem Th20: :: TOPREAL7:20
for M, N being non empty Reflexive MetrStruct holds max-Prod2 (M,N) is Reflexive
proofend;

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
proofend;

theorem Th21: :: TOPREAL7:21
for M, N being non empty symmetric MetrStruct holds max-Prod2 (M,N) is symmetric
proofend;

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
proofend;

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))
proofend;

theorem :: TOPREAL7:24
for M, N being non empty MetrSpace st the carrier of M = the carrier of N &amp; ( for m being Point of M
for n being Point of N
for r being Real st r > 0 &amp; m = n holds
ex r1 being Real st
( r1 > 0 &amp; Ball (n,r1) c= Ball (m,r) ) ) &amp; ( for m being Point of M
for n being Point of N
for r being Real st r > 0 &amp; m = n holds
ex r1 being Real st
( r1 > 0 &amp; Ball (m,r1) c= Ball (n,r) ) ) holds
TopSpaceMetr M = TopSpaceMetr N
proofend;

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 &amp; ( for fi, fj being FinSequence st [fi,fj] in dom f holds
f . (fi,fj) = fi ^ fj ) )
proofend;

theorem :: TOPREAL7:25
for i, j being Element of NAT holds [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], TopSpaceMetr (Euclid (i + j)) are_homeomorphic
proofend;

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 &amp; ( for fi, fj being FinSequence st [fi,fj] in dom f holds
f . (fi,fj) = fi ^ fj ) ) by Lm2;