:: TOPREAL7 semantic presentation

theorem Th1: :: TOPREAL7:1
for b1, b2 being Real st max b1,b2 <= b1 holds
max b1,b2 = b1
proof end;

theorem Th2: :: TOPREAL7:2
for b1, b2, b3, b4 being Real holds max (b1 + b3),(b2 + b4) <= (max b1,b2) + (max b3,b4)
proof end;

theorem Th3: :: TOPREAL7:3
for b1, b2, b3, b4, b5, b6 being Real st b1 <= b2 + b3 & b4 <= b5 + b6 holds
max b1,b4 <= (max b2,b5) + (max b3,b6)
proof end;

theorem Th4: :: TOPREAL7:4
for b1, b2 being FinSequence holds dom b2 c= dom (b1 ^ b2)
proof end;

theorem Th5: :: TOPREAL7:5
for b1 being Nat
for b2, b3 being FinSequence st len b2 < b1 & b1 <= (len b2) + (len b3) holds
b1 - (len b2) in dom b3
proof end;

theorem Th6: :: TOPREAL7:6
for b1, b2, b3, b4 being FinSequence st b1 ^ b2 = b3 ^ b4 & len b1 = len b3 & len b2 = len b4 holds
( b1 = b3 & b2 = b4 )
proof end;

theorem Th7: :: TOPREAL7:7
for b1, b2 being FinSequence of REAL st ( len b1 = len b2 or dom b1 = dom b2 ) holds
( len (b1 + b2) = len b1 & dom (b1 + b2) = dom b1 )
proof end;

theorem Th8: :: TOPREAL7:8
for b1, b2 being FinSequence of REAL st ( len b1 = len b2 or dom b1 = dom b2 ) holds
( len (b1 - b2) = len b1 & dom (b1 - b2) = dom b1 )
proof end;

theorem Th9: :: TOPREAL7:9
for b1 being FinSequence of REAL holds
( len b1 = len (sqr b1) & dom b1 = dom (sqr b1) )
proof end;

theorem Th10: :: TOPREAL7:10
for b1 being FinSequence of REAL holds
( len b1 = len (abs b1) & dom b1 = dom (abs b1) )
proof end;

theorem Th11: :: TOPREAL7:11
for b1, b2 being FinSequence of REAL holds sqr (b1 ^ b2) = (sqr b1) ^ (sqr b2)
proof end;

theorem Th12: :: TOPREAL7:12
for b1, b2 being FinSequence of REAL holds abs (b1 ^ b2) = (abs b1) ^ (abs b2)
proof end;

theorem Th13: :: TOPREAL7:13
for b1, b2, b3, b4 being FinSequence of REAL st len b1 = len b2 & len b3 = len b4 holds
sqr ((b1 ^ b3) + (b2 ^ b4)) = (sqr (b1 + b2)) ^ (sqr (b3 + b4))
proof end;

theorem Th14: :: TOPREAL7:14
for b1, b2, b3, b4 being FinSequence of REAL st len b1 = len b2 & len b3 = len b4 holds
abs ((b1 ^ b3) + (b2 ^ b4)) = (abs (b1 + b2)) ^ (abs (b3 + b4))
proof end;

theorem Th15: :: TOPREAL7:15
for b1, b2, b3, b4 being FinSequence of REAL st len b1 = len b2 & len b3 = len b4 holds
sqr ((b1 ^ b3) - (b2 ^ b4)) = (sqr (b1 - b2)) ^ (sqr (b3 - b4))
proof end;

theorem Th16: :: TOPREAL7:16
for b1, b2, b3, b4 being FinSequence of REAL st len b1 = len b2 & len b3 = len b4 holds
abs ((b1 ^ b3) - (b2 ^ b4)) = (abs (b1 - b2)) ^ (abs (b3 - b4))
proof end;

theorem Th17: :: TOPREAL7:17
for b1 being Nat
for b2 being FinSequence of REAL st len b2 = b1 holds
b2 in the carrier of (Euclid b1)
proof end;

theorem Th18: :: TOPREAL7:18
for b1 being Nat
for b2 being FinSequence of REAL st len b2 = b1 holds
b2 in the carrier of (TOP-REAL b1)
proof end;

theorem Th19: :: TOPREAL7:19
for b1 being Nat
for b2 being FinSequence st b2 in the carrier of (Euclid b1) holds
len b2 = b1 by FINSEQ_2:109;

definition
let c1, c2 be non empty MetrStruct ;
func max-Prod2 c1,c2 -> strict MetrStruct means :Def1: :: TOPREAL7:def 1
( the carrier of a3 = [:the carrier of a1,the carrier of a2:] & ( for b1, b2 being Point of a3 ex b3, b4 being Point of a1ex b5, b6 being Point of a2 st
( b1 = [b3,b5] & b2 = [b4,b6] & the distance of a3 . b1,b2 = max (the distance of a1 . b3,b4),(the distance of a2 . b5,b6) ) ) );
existence
ex b1 being strict MetrStruct st
( the carrier of b1 = [:the carrier of c1,the carrier of c2:] & ( for b2, b3 being Point of b1 ex b4, b5 being Point of c1ex b6, b7 being Point of c2 st
( b2 = [b4,b6] & b3 = [b5,b7] & the distance of b1 . b2,b3 = max (the distance of c1 . b4,b5),(the distance of c2 . b6,b7) ) ) )
proof end;
uniqueness
for b1, b2 being strict MetrStruct st the carrier of b1 = [:the carrier of c1,the carrier of c2:] & ( for b3, b4 being Point of b1 ex b5, b6 being Point of c1ex b7, b8 being Point of c2 st
( b3 = [b5,b7] & b4 = [b6,b8] & the distance of b1 . b3,b4 = max (the distance of c1 . b5,b6),(the distance of c2 . b7,b8) ) ) & the carrier of b2 = [:the carrier of c1,the carrier of c2:] & ( for b3, b4 being Point of b2 ex b5, b6 being Point of c1ex b7, b8 being Point of c2 st
( b3 = [b5,b7] & b4 = [b6,b8] & the distance of b2 . b3,b4 = max (the distance of c1 . b5,b6),(the distance of c2 . b7,b8) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines max-Prod2 TOPREAL7:def 1 :
for b1, b2 being non empty MetrStruct
for b3 being strict MetrStruct holds
( b3 = max-Prod2 b1,b2 iff ( the carrier of b3 = [:the carrier of b1,the carrier of b2:] & ( for b4, b5 being Point of b3 ex b6, b7 being Point of b1ex b8, b9 being Point of b2 st
( b4 = [b6,b8] & b5 = [b7,b9] & the distance of b3 . b4,b5 = max (the distance of b1 . b6,b7),(the distance of b2 . b8,b9) ) ) ) );

registration
let c1, c2 be non empty MetrStruct ;
cluster max-Prod2 a1,a2 -> non empty strict ;
coherence
not max-Prod2 c1,c2 is empty
proof end;
end;

definition
let c1, c2 be non empty MetrStruct ;
let c3 be Point of c1;
let c4 be Point of c2;
redefine func [ as [c3,c4] -> Element of (max-Prod2 a1,a2);
coherence
[c3,c4] is Element of (max-Prod2 c1,c2)
proof end;
end;

definition
let c1, c2 be non empty MetrStruct ;
let c3 be Point of (max-Prod2 c1,c2);
redefine func `1 as c3 `1 -> Element of a1;
coherence
c3 `1 is Element of c1
proof end;
redefine func `2 as c3 `2 -> Element of a2;
coherence
c3 `2 is Element of c2
proof end;
end;

theorem Th20: :: TOPREAL7:20
for b1, b2 being non empty MetrStruct
for b3, b4 being Point of b1
for b5, b6 being Point of b2 holds dist [b3,b5],[b4,b6] = max (dist b3,b4),(dist b5,b6)
proof end;

theorem Th21: :: TOPREAL7:21
for b1, b2 being non empty MetrStruct
for b3, b4 being Point of (max-Prod2 b1,b2) holds dist b3,b4 = max (dist (b3 `1 ),(b4 `1 )),(dist (b3 `2 ),(b4 `2 ))
proof end;

theorem Th22: :: TOPREAL7:22
for b1, b2 being non empty Reflexive MetrStruct holds max-Prod2 b1,b2 is Reflexive
proof end;

registration
let c1, c2 be non empty Reflexive MetrStruct ;
cluster max-Prod2 a1,a2 -> non empty strict Reflexive ;
coherence
max-Prod2 c1,c2 is Reflexive by Th22;
end;

Lemma17: for b1, b2 being non empty MetrSpace holds max-Prod2 b1,b2 is discerning
proof end;

theorem Th23: :: TOPREAL7:23
for b1, b2 being non empty symmetric MetrStruct holds max-Prod2 b1,b2 is symmetric
proof end;

registration
let c1, c2 be non empty symmetric MetrStruct ;
cluster max-Prod2 a1,a2 -> non empty strict symmetric ;
coherence
max-Prod2 c1,c2 is symmetric by Th23;
end;

theorem Th24: :: TOPREAL7:24
for b1, b2 being non empty triangle MetrStruct holds max-Prod2 b1,b2 is triangle
proof end;

registration
let c1, c2 be non empty triangle MetrStruct ;
cluster max-Prod2 a1,a2 -> non empty strict triangle ;
coherence
max-Prod2 c1,c2 is triangle by Th24;
end;

registration
let c1, c2 be non empty MetrSpace;
cluster max-Prod2 a1,a2 -> non empty strict Reflexive discerning symmetric triangle ;
coherence
max-Prod2 c1,c2 is discerning by Lemma17;
end;

theorem Th25: :: TOPREAL7:25
for b1, b2 being non empty MetrSpace holds [:(TopSpaceMetr b1),(TopSpaceMetr b2):] = TopSpaceMetr (max-Prod2 b1,b2)
proof end;

theorem Th26: :: TOPREAL7:26
for b1, b2 being non empty MetrSpace st the carrier of b1 = the carrier of b2 & ( for b3 being Point of b1
for b4 being Point of b2
for b5 being Real st b5 > 0 & b3 = b4 holds
ex b6 being Real st
( b6 > 0 & Ball b4,b6 c= Ball b3,b5 ) ) & ( for b3 being Point of b1
for b4 being Point of b2
for b5 being Real st b5 > 0 & b3 = b4 holds
ex b6 being Real st
( b6 > 0 & Ball b3,b6 c= Ball b4,b5 ) ) holds
TopSpaceMetr b1 = TopSpaceMetr b2
proof end;

theorem Th27: :: TOPREAL7:27
for b1, b2 being Nat holds [:(TOP-REAL b1),(TOP-REAL b2):], TOP-REAL (b1 + b2) are_homeomorphic
proof end;