:: JORDAN2B semantic presentation

Lemma1: for b₁, b₂ being Nat
for b₃ being Element of (TOP-REAL b₁) ex b₄ being Realex b₅ being FinSequence of REAL st
( b₅ = b₃ & b₄ = b₅ /. b₂ )

proof end;

Lemma2: for b₁, b₂ being Nat
for b₃ being Element of (TOP-REAL b₁) ex b₄ being Real st
for b₅ being FinSequence of REAL st b₅ = b₃ holds
b₄ = b₅ /. b₂

proof end;

definition

let c₁, c₂ be Nat;
let c₃ be Element of (TOP-REAL c₁);
func Proj c₃,c₂ -> Real means :Def1: :: JORDAN2B:def 1
for b₁ being FinSequence of REAL st b₁ = a₃ holds
a₄ = b₁ /. a₂;
existence by Lemma2;
uniqueness

proof end;

end;

:: deftheorem Def1 defines Proj JORDAN2B:def 1 :

theorem Th1: :: JORDAN2B:1

for b₁, b₂ being Nat ex b₃ being Function of (TOP-REAL b₁),R^1 st
for b₄ being Element of (TOP-REAL b₁) holds b₃ . b₄ = Proj b₄,b₂

proof end;

theorem Th2: :: JORDAN2B:2

for b₁, b₂ being Nat st b₂ in Seg b₁ holds
(0* b₁) . b₂ = 0

proof end;

theorem Th3: :: JORDAN2B:3

for b₁, b₂ being Nat st b₂ in Seg b₁ holds
Proj (0.REAL b₁),b₂ = 0

proof end;

theorem Th4: :: JORDAN2B:4

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁)
for b₄ being Nat st b₄ in Seg b₁ holds
Proj (b₂ * b₃),b₄ = b₂ * (Proj b₃,b₄)

proof end;

theorem Th5: :: JORDAN2B:5

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁)
for b₃ being Nat st b₃ in Seg b₁ holds
Proj (- b₂),b₃ = - (Proj b₂,b₃)

proof end;

theorem Th6: :: JORDAN2B:6

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄ being Nat st b₄ in Seg b₁ holds
Proj (b₂ + b₃),b₄ = (Proj b₂,b₄) + (Proj b₃,b₄)

proof end;

theorem Th7: :: JORDAN2B:7

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄ being Nat st b₄ in Seg b₁ holds
Proj (b₂ - b₃),b₄ = (Proj b₂,b₄) - (Proj b₃,b₄)

proof end;

theorem Th8: :: JORDAN2B:8

for b₁ being Nat holds len (0* b₁) = b₁ by FINSEQ_2:109;

theorem Th9: :: JORDAN2B:9

for b₁, b₂ being Nat st b₁ <= b₂ holds
(0* b₂) | b₁ = 0* b₁

proof end;

theorem Th10: :: JORDAN2B:10

for b₁, b₂ being Nat holds (0* b₁) /^ b₂ = 0* (b₁ -' b₂)

proof end;

theorem Th11: :: JORDAN2B:11

for b₁ being Nat holds Sum (0* b₁) = 0

proof end;

theorem Th12: :: JORDAN2B:12

for b₁ being FinSequence
for b₂ being set
for b₃ being Nat holds len (b₁ +* b₃,b₂) = len b₁

proof end;

theorem Th13: :: JORDAN2B:13

for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂
for b₄ being Element of b₂ st b₁ in dom b₃ holds
b₃ +* b₁,b₄ = ((b₃ | (b₁ -' 1)) ^ <*b₄*>) ^ (b₃ /^ b₁)

proof end;

theorem Th14: :: JORDAN2B:14

for b₁, b₂ being Nat
for b₃ being Real st b₁ in Seg b₂ holds
Sum ((0* b₂) +* b₁,b₃) = b₃

proof end;

theorem Th15: :: JORDAN2B:15

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃ being Point of (TOP-REAL b₁)
for b₄ being Nat st b₄ in Seg b₁ & b₂ = b₃ holds
( Proj b₃,b₄ <= |.b₂.| & (Proj b₃,b₄) ^2 <= |.b₂.| ^2 )

proof end;

theorem Th16: :: JORDAN2B:16

for b₁ being Nat
for b₂ being real number
for b₃ being Subset of (TOP-REAL b₁)
for b₄ being Nat st b₃ = { b₅ where B is Point of (TOP-REAL b₁) : b₂ > Proj b₅,b₄ } & b₄ in Seg b₁ holds
b₃ is open

proof end;

theorem Th17: :: JORDAN2B:17

for b₁ being Nat
for b₂ being real number
for b₃ being Subset of (TOP-REAL b₁)
for b₄ being Nat st b₃ = { b₅ where B is Point of (TOP-REAL b₁) : b₂ < Proj b₅,b₄ } & b₄ in Seg b₁ holds
b₃ is open

proof end;

theorem Th18: :: JORDAN2B:18

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄ being real number
for b₅ being Nat st b₂ = { b₆ where B is Element of (TOP-REAL b₁) : ( b₃ < Proj b₆,b₅ & Proj b₆,b₅ < b₄ ) } & b₅ in Seg b₁ holds
b₂ is open

proof end;

theorem Th19: :: JORDAN2B:19

for b₁ being Nat
for b₂, b₃ being real number
for b₄ being Function of (TOP-REAL b₁),R^1
for b₅ being Nat st ( for b₆ being Element of (TOP-REAL b₁) holds b₄ . b₆ = Proj b₆,b₅ ) holds
b₄ " { b₆ where B is Real : ( b₂ < b₆ & b₆ < b₃ ) } = { b₆ where B is Element of (TOP-REAL b₁) : ( b₂ < Proj b₆,b₅ & Proj b₆,b₅ < b₃ ) }

proof end;

theorem Th20: :: JORDAN2B:20

for b₁ being non empty TopSpace
for b₂ being non empty MetrSpace
for b₃ being Function of b₁,(TopSpaceMetr b₂) st ( for b₄ being real number
for b₅ being Element of the carrier of b₂
for b₆ being Subset of (TopSpaceMetr b₂) st b₄ > 0 & b₆ = Ball b₅,b₄ holds
b₃ " b₆ is open ) holds
b₃ is continuous

proof end;

theorem Th21: :: JORDAN2B:21

for b₁ being Point of RealSpace
for b₂, b₃ being real number st b₃ = b₁ & b₂ > 0 holds
Ball b₁,b₂ = { b₄ where B is Real : ( b₃ - b₂ < b₄ & b₄ < b₃ + b₂ ) }

proof end;

theorem Th22: :: JORDAN2B:22

for b₁ being Nat
for b₂ being Function of (TOP-REAL b₁),R^1
for b₃ being Nat st b₃ in Seg b₁ & ( for b₄ being Element of (TOP-REAL b₁) holds b₂ . b₄ = Proj b₄,b₃ ) holds
b₂ is continuous

proof end;

theorem Th23: :: JORDAN2B:23

for b₁ being Real holds abs <*b₁*> = <*(abs b₁)*>

proof end;

theorem Th24: :: JORDAN2B:24

for b₁ being Element of (TOP-REAL 1) ex b₂ being Real st b₁ = <*b₂*>

proof end;

theorem Th25: :: JORDAN2B:25

for b₁ being Element of (Euclid 1) ex b₂ being Real st b₁ = <*b₂*> by FINSEQ_2:117;

definition

let c₁ be real number ;
func |[c₁]| -> Point of (TOP-REAL 1) equals :: JORDAN2B:def 2
<*a₁*>;
coherence

proof end;

end;

:: deftheorem Def2 defines |[ JORDAN2B:def 2 :

theorem Th26: :: JORDAN2B:26

for b₁ being real number
for b₂ being Real holds b₂ * |[b₁]| = |[(b₂ * b₁)]|

proof end;

theorem Th27: :: JORDAN2B:27

for b₁, b₂ being real number holds |[(b₁ + b₂)]| = |[b₁]| + |[b₂]|

proof end;

theorem Th28: :: JORDAN2B:28

|[0]| = 0.REAL 1 by FINSEQ_2:73;

theorem Th29: :: JORDAN2B:29

for b₁, b₂ being real number st |[b₁]| = |[b₂]| holds
b₁ = b₂

proof end;

theorem Th30: :: JORDAN2B:30

for b₁ being Subset of R^1
for b₂ being real number st b₁ = { b₃ where B is Real : b₃ < b₂ } holds
b₁ is open

proof end;

theorem Th31: :: JORDAN2B:31

for b₁ being Subset of R^1
for b₂ being real number st b₁ = { b₃ where B is Real : b₂ < b₃ } holds
b₁ is open

proof end;

theorem Th32: :: JORDAN2B:32

for b₁ being Subset of R^1
for b₂, b₃ being real number st b₁ = { b₄ where B is Real : ( b₂ < b₄ & b₄ < b₃ ) } holds
b₁ is open

proof end;

theorem Th33: :: JORDAN2B:33

for b₁ being Point of (Euclid 1)
for b₂, b₃ being real number st <*b₃*> = b₁ & b₂ > 0 holds
Ball b₁,b₂ = { <*b₄*> where B is Real : ( b₃ - b₂ < b₄ & b₄ < b₃ + b₂ ) }

proof end;

theorem Th34: :: JORDAN2B:34

for b₁ being Function of (TOP-REAL 1),R^1 st ( for b₂ being Element of (TOP-REAL 1) holds b₁ . b₂ = Proj b₂,1 ) holds
b₁ is_homeomorphism

proof end;

theorem Th35: :: JORDAN2B:35

for b₁ being Element of (TOP-REAL 2) holds
( Proj b₁,1 = b₁ `1 & Proj b₁,2 = b₁ `2 )

proof end;

theorem Th36: :: JORDAN2B:36

for b₁ being Element of (TOP-REAL 2) holds
( Proj b₁,1 = proj1 . b₁ & Proj b₁,2 = proj2 . b₁ )

proof end;