:: EUCLID semantic presentation

begin


definition
let n be Nat;
func REAL n ->  FinSequenceSet of REAL  equals :: EUCLID:def 1
n -tuples_on REAL;
coherence
 n -tuples_on REAL is FinSequenceSet of REAL ;
end;

:: deftheorem  defines REAL EUCLID:def_1_:_
 for n being Nat holds REAL n = n -tuples_on REAL;

registration
let n be Nat;
cluster REAL n ->  non empty ;
coherence
 not REAL n is empty ;
end;

registration
let n be Nat;
cluster  -> n -element for Element of REAL n;
coherence
 for b1 being Element of REAL n holds b1 is n -element ;
end;

definition
func absreal  ->  Function of REAL,REAL means :Def2: :: EUCLID:def 2
 for r being real number holds it . r = abs r;
existence
 ex b1 being Function of REAL,REAL st
for r being real number holds b1 . r = abs r
proof
deffunc H1( Real) ->  Element of REAL = abs $1;
consider f being Function of REAL,REAL such that
A1: for r being Real holds f . r = H1(r) from FUNCT_2:sch_4();
take  f ; ::_thesis: for r being real number holds f . r = abs r
let r be real number ; ::_thesis: f . r = abs r
 r is Real by XREAL_0:def_1;
hence  f . r = abs r by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of REAL,REAL st ( for r being real number holds b1 . r = abs r ) & ( for r being real number holds b2 . r = abs r ) holds
b1 = b2
proof
let f, g be Function of REAL,REAL; ::_thesis: ( ( for r being real number holds f . r = abs r ) & ( for r being real number holds g . r = abs r ) implies f = g )
assume that
A2: for r being real number holds f . r = abs r and
A3: for r being real number holds g . r = abs r ; ::_thesis: f = g
now__::_thesis:_for_x_being_Element_of_REAL_holds_f_._x_=_g_._x
let x be Element of REAL ; ::_thesis: f . x = g . x
thus f . x = abs x by A2
.= g . x by A3 ; ::_thesis: verum
end;
hence  f = g by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines absreal EUCLID:def_2_:_
 for b1 being Function of REAL,REAL holds
( b1 = absreal iff for r being real number holds b1 . r = abs r );

definition
let x be real-valued FinSequence;
:: original: |.
redefine func abs x ->  FinSequence of REAL  equals :: EUCLID:def 3
absreal * x;
coherence
 |.x.| is FinSequence of REAL
proof
thus  rng (abs x) c= REAL ; :: according to FINSEQ_1:def_4 ::_thesis: verum
end;
compatibility
 for b1 being FinSequence of REAL holds
( b1 = |.x.| iff b1 = absreal * x )
proof
set g = absreal * x;
 dom absreal = REAL by FUNCT_2:def_1;
then  rng x c= dom absreal ;
then A1: ( dom (abs x) = dom x & dom (absreal * x) = dom x ) by RELAT_1:27, VALUED_1:def_11;
now__::_thesis:_for_a_being_set_st_a_in_dom_(abs_x)_holds_
(abs_x)_._a_=_(absreal_*_x)_._a
let a be set ; ::_thesis: ( a in dom (abs x) implies (abs x) . a = (absreal * x) . a )
assume A2: a in dom (abs x) ; ::_thesis: (abs x) . a = (absreal * x) . a
thus (abs x) . a = abs (x . a) by VALUED_1:18
.= absreal . (x . a) by Def2
.= (absreal * x) . a by A1, A2, FUNCT_1:12 ; ::_thesis: verum
end;
hence  for b1 being FinSequence of REAL holds
( b1 = |.x.| iff b1 = absreal * x ) by A1, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem  defines abs EUCLID:def_3_:_
 for x being real-valued FinSequence holds abs x = absreal * x;

definition
let n be Nat;
func 0* n ->  real-valued FinSequence equals :: EUCLID:def 4
n |-> 0;
coherence
 n |-> 0 is real-valued FinSequence ;
end;

:: deftheorem  defines 0* EUCLID:def_4_:_
 for n being Nat holds 0* n = n |-> 0;

definition
let n be Nat;
:: original: 0*
redefine func 0* n ->  Element of REAL n;
coherence
 0* n is Element of REAL n ;
end;


definition
let n be Nat;
let x be Element of REAL n;
:: original: -
redefine func - x ->  Element of REAL n;
coherence
 - x is Element of REAL n
proof
reconsider n = n as Element of NAT by ORDINAL1:def_12;
reconsider R1 = x as Element of n -tuples_on REAL ;
 - R1 in n -tuples_on REAL ;
hence  - x is Element of REAL n ; ::_thesis: verum
end;
end;

definition
let n be Nat;
let x, y be Element of REAL n;
:: original: +
redefine funcx + y ->  Element of REAL n;
coherence
 x + y is Element of REAL n
proof
reconsider n = n as Element of NAT by ORDINAL1:def_12;
reconsider R1 = x, R2 = y as Element of n -tuples_on REAL ;
 R1 + R2 in n -tuples_on REAL ;
hence  x + y is Element of REAL n ; ::_thesis: verum
end;
:: original: -
redefine funcx - y ->  Element of REAL n;
coherence
 x - y is Element of REAL n
proof
reconsider n = n as Element of NAT by ORDINAL1:def_12;
reconsider R1 = x, R2 = y as Element of n -tuples_on REAL ;
 R1 - R2 in n -tuples_on REAL ;
hence  x - y is Element of REAL n ; ::_thesis: verum
end;
end;

definition
let n be Nat;
let x be Element of REAL n;
let r be real number ;
:: original: (#)
redefine funcr * x ->  Element of REAL n;
coherence
 r (#) x is Element of REAL n
proof
reconsider n = n as Element of NAT by ORDINAL1:def_12;
reconsider R = x as Element of n -tuples_on REAL ;
 r * R in n -tuples_on REAL ;
hence  r (#) x is Element of REAL n ; ::_thesis: verum
end;
end;

definition
let n be Nat;
let x be Element of REAL n;
:: original: |.
redefine func abs x ->  Element of n -tuples_on REAL;
coherence
 |.x.| is Element of n -tuples_on REAL by FINSEQ_2:113;
end;

definition
let n be Nat;
let x be Element of REAL n;
:: original: ^2
redefine func sqr x ->  Element of n -tuples_on REAL;
coherence
 x ^2 is Element of n -tuples_on REAL by FINSEQ_2:113;
end;

definition
let f be real-valued FinSequence;
func|.f.| ->  Real equals :: EUCLID:def 5
 sqrt (Sum (sqr f));
coherence
 sqrt (Sum (sqr f)) is Real ;
end;

:: deftheorem  defines |. EUCLID:def_5_:_
 for f being real-valued FinSequence holds |.f.| = sqrt (Sum (sqr f));

Lm1:  for f being real-valued FinSequence holds f is Element of REAL (len f)
proof
let f be real-valued FinSequence; ::_thesis: f is Element of REAL (len f)
 rng f c= REAL ;
then  f is FinSequence of REAL by FINSEQ_1:def_4;
then  f is Element of REAL * by FINSEQ_1:def_11;
then  f in (len f) -tuples_on REAL ;
hence  f is Element of REAL (len f) ; ::_thesis: verum
end;

theorem :: EUCLID:1
canceled;

theorem :: EUCLID:2
canceled;

theorem :: EUCLID:3
canceled;

theorem :: EUCLID:4
for n being Nat holds abs (0* n) = n |-> 0
proof
let n be Nat; ::_thesis: abs (0* n) = n |-> 0
reconsider m = n as Element of NAT by ORDINAL1:def_12;
thus  abs (0* n) = m |-> (absreal . 0) by FINSEQOP:16
.= n |-> (abs 0) by Def2
.= n |-> 0 by ABSVALUE:2 ; ::_thesis: verum
end;

theorem Th5: :: EUCLID:5
for f being complex-valued Function holds abs (- f) = abs f
proof
let f be complex-valued Function; ::_thesis: abs (- f) = abs f
A1: dom (abs (- f)) = dom (- f) by VALUED_1:def_11;
A2: dom (abs f) = dom f by VALUED_1:def_11;
A3: dom (- f) = dom f by VALUED_1:8;
now__::_thesis:_for_x_being_set_st_x_in_dom_(abs_(-_f))_holds_
(abs_(-_f))_._x_=_(abs_f)_._x
let x be set ; ::_thesis: ( x in dom (abs (- f)) implies (abs (- f)) . x = (abs f) . x )
assume  x in dom (abs (- f)) ; ::_thesis: (abs (- f)) . x = (abs f) . x
thus (abs (- f)) . x = abs ((- f) . x) by VALUED_1:18
.= abs (- (f . x)) by VALUED_1:8
.= abs (f . x) by COMPLEX1:52
.= (abs f) . x by VALUED_1:18 ; ::_thesis: verum
end;
hence  abs (- f) = abs f by A1, A2, A3, FUNCT_1:2; ::_thesis: verum
end;

theorem Th6: :: EUCLID:6
for r being real number
for f being real-valued FinSequence holds abs (r * f) = (abs r) * (abs f) by RFUNCT_1:25;

theorem Th7: :: EUCLID:7
for n being Nat holds |.(0* n).| = 0
proof
let n be Nat; ::_thesis: |.(0* n).| = 0
thus |.(0* n).| = sqrt (Sum (n |-> (0 ^2))) by RVSUM_1:56
.= sqrt (n * 0) by RVSUM_1:80
.= 0 by SQUARE_1:17 ; ::_thesis: verum
end;

Lm2:  for f being real-valued FinSequence holds sqr (abs f) = sqr f
proof
let f be real-valued FinSequence; ::_thesis: sqr (abs f) = sqr f
set n = len f;
reconsider x = f as Element of REAL (len f) by Lm1;
now__::_thesis:_for_k_being_Nat_st_k_in_Seg_(len_f)_holds_
(sqr_(abs_x))_._k_=_(sqr_x)_._k
let k be Nat; ::_thesis: ( k in Seg (len f) implies (sqr (abs x)) . k = (sqr x) . k )
assume  k in Seg (len f) ; ::_thesis: (sqr (abs x)) . k = (sqr x) . k
thus (sqr (abs x)) . k = ((abs x) . k) ^2 by VALUED_1:11
.= (abs (x . k)) ^2 by VALUED_1:18
.= (x . k) ^2 by COMPLEX1:75
.= (sqr x) . k by VALUED_1:11 ; ::_thesis: verum
end;
hence  sqr (abs f) = sqr f by FINSEQ_2:119; ::_thesis: verum
end;

theorem Th8: :: EUCLID:8
for n being Nat
for x being Element of REAL n st |.x.| = 0 holds
x = 0* n
proof
let n be Nat; ::_thesis: for x being Element of REAL n st |.x.| = 0 holds
x = 0* n
let x be Element of REAL n; ::_thesis: ( |.x.| = 0 implies x = 0* n )
assume A1: |.x.| = 0 ; ::_thesis: x = 0* n
now__::_thesis:_for_j_being_Nat_st_j_in_Seg_n_holds_
x_._j_=_(n_|->_0)_._j
let j be Nat; ::_thesis: ( j in Seg n implies x . j = (n |-> 0) . j )
assume  j in Seg n ; ::_thesis: x . j = (n |-> 0) . j
reconsider r = x . j as Element of REAL ;
 Sum (sqr x) = 0 by A1, RVSUM_1:86, SQUARE_1:24;
then  Sum (sqr (abs x)) = 0 by Lm2;
then  (abs x) . j = (n |-> 0) . j by RVSUM_1:91;
then  abs r = (n |-> 0) . j by VALUED_1:18;
then  abs r = 0 ;
then  r = 0 by ABSVALUE:2;
hence  x . j = (n |-> 0) . j ; ::_thesis: verum
end;
hence  x = 0* n by FINSEQ_2:119; ::_thesis: verum
end;

theorem Th9: :: EUCLID:9
for f being real-valued FinSequence holds |.f.| >= 0
proof
let f be real-valued FinSequence; ::_thesis: |.f.| >= 0
 0 <= Sum (sqr f) by RVSUM_1:86;
hence  |.f.| >= 0 by SQUARE_1:def_2; ::_thesis: verum
end;

registration
let f be real-valued FinSequence;
cluster|.f.| ->  non negative ;
coherence
 not |.f.| is negative by Th9;
end;

theorem Th10: :: EUCLID:10
for f being real-valued FinSequence holds |.(- f).| = |.f.|
proof
let f be real-valued FinSequence; ::_thesis: |.(- f).| = |.f.|
thus |.(- f).| = sqrt (Sum (sqr (abs (- f)))) by Lm2
.= sqrt (Sum (sqr (abs f))) by Th5
.= |.f.| by Lm2 ; ::_thesis: verum
end;

theorem :: EUCLID:11
for r being real number
for f being real-valued FinSequence holds |.(r * f).| = (abs r) * |.f.|
proof
let r be real number ; ::_thesis: for f being real-valued FinSequence holds |.(r * f).| = (abs r) * |.f.|
let f be real-valued FinSequence; ::_thesis: |.(r * f).| = (abs r) * |.f.|
set n = len f;
reconsider x = f as Element of REAL (len f) by Lm1;
A1: ( 0 <= (abs r) ^2 & 0 <= Sum (sqr (abs x)) ) by RVSUM_1:86, XREAL_1:63;
thus |.(r * f).| = sqrt (Sum (sqr (abs (r * x)))) by Lm2
.= sqrt (Sum (sqr ((abs r) * (abs x)))) by Th6
.= sqrt (Sum (((abs r) ^2) * (sqr (abs x)))) by RVSUM_1:58
.= sqrt (((abs r) ^2) * (Sum (sqr (abs x)))) by RVSUM_1:87
.= (sqrt ((abs r) ^2)) * (sqrt (Sum (sqr (abs x)))) by A1, SQUARE_1:29
.= (abs r) * (sqrt (Sum (sqr (abs x)))) by COMPLEX1:46, SQUARE_1:22
.= (abs r) * |.f.| by Lm2 ; ::_thesis: verum
end;

theorem Th12: :: EUCLID:12
for n being Nat
for x1, x2 being Element of REAL n holds |.(x1 + x2).| <= |.x1.| + |.x2.|
proof
let n be Nat; ::_thesis: for x1, x2 being Element of REAL n holds |.(x1 + x2).| <= |.x1.| + |.x2.|
let x1, x2 be Element of REAL n; ::_thesis: |.(x1 + x2).| <= |.x1.| + |.x2.|
A1: 0 <= Sum (sqr (x1 + x2)) by RVSUM_1:86;
A2: 0 <= Sum (sqr (abs x1)) by RVSUM_1:86;
then A3: 0 <= sqrt (Sum (sqr (abs x1))) by SQUARE_1:def_2;
A4: for k being Nat st k in Seg n holds
(sqr (abs (x1 + x2))) . k <= (sqr ((abs x1) + (abs x2))) . k
proof
let k be Nat; ::_thesis: ( k in Seg n implies (sqr (abs (x1 + x2))) . k <= (sqr ((abs x1) + (abs x2))) . k )
 len (x1 + x2) = n by CARD_1:def_7;
then A5: dom (x1 + x2) = Seg n by FINSEQ_1:def_3;
assume A6: k in Seg n ; ::_thesis: (sqr (abs (x1 + x2))) . k <= (sqr ((abs x1) + (abs x2))) . k
reconsider abs1 = (abs x1) . k, abs2 = (abs x2) . k as Real ;
reconsider r12 = (x1 + x2) . k as Element of REAL ;
reconsider r11 = x1 . k, r22 = x2 . k as Element of REAL ;
 abs (r11 + r22) <= (abs r11) + (abs r22) by COMPLEX1:56;
then  abs r12 <= (abs r11) + (abs r22) by A6, A5, VALUED_1:def_1;
then  abs r12 <= (abs r11) + abs2 by VALUED_1:18;
then A7: abs r12 <= abs1 + abs2 by VALUED_1:18;
reconsider abs912 = (abs (x1 + x2)) . k as Real ;
reconsider abs12 = ((abs x1) + (abs x2)) . k as Real ;
set r2 = (sqr ((abs x1) + (abs x2))) . k;
 abs r12 >= 0 by COMPLEX1:46;
then A8: 0 <= abs912 by VALUED_1:18;
 len ((abs x1) + (abs x2)) = n by CARD_1:def_7;
then  dom ((abs x1) + (abs x2)) = Seg n by FINSEQ_1:def_3;
then  abs r12 <= abs12 by A6, A7, VALUED_1:def_1;
then  abs912 <= abs12 by VALUED_1:18;
then  abs912 ^2 <= abs12 ^2 by A8, SQUARE_1:15;
then  abs912 ^2 <= (sqr ((abs x1) + (abs x2))) . k by VALUED_1:11;
hence  (sqr (abs (x1 + x2))) . k <= (sqr ((abs x1) + (abs x2))) . k by VALUED_1:11; ::_thesis: verum
end;
 0 <= (Sum (mlt ((abs x1),(abs x2)))) ^2 by XREAL_1:63;
then A9: sqrt ((Sum (mlt ((abs x1),(abs x2)))) ^2) <= sqrt ((Sum (sqr (abs x1))) * (Sum (sqr (abs x2)))) by RVSUM_1:92, SQUARE_1:26;
A10: for k being Nat st k in Seg n holds
0 <= (mlt ((abs x1),(abs x2))) . k
proof
let k be Nat; ::_thesis: ( k in Seg n implies 0 <= (mlt ((abs x1),(abs x2))) . k )
assume  k in Seg n ; ::_thesis: 0 <= (mlt ((abs x1),(abs x2))) . k
set r = (mlt ((abs x1),(abs x2))) . k;
reconsider r1 = x1 . k, r2 = x2 . k as Element of REAL ;
 ( (abs x1) . k = abs r1 & (abs x2) . k = abs r2 ) by VALUED_1:18;
then A11: (mlt ((abs x1),(abs x2))) . k = (abs r1) * (abs r2) by RVSUM_1:60;
 ( 0 <= abs r1 & 0 <= abs r2 ) by COMPLEX1:46;
hence  0 <= (mlt ((abs x1),(abs x2))) . k by A11; ::_thesis: verum
end;
 len (mlt ((abs x1),(abs x2))) = n by CARD_1:def_7;
then  dom (mlt ((abs x1),(abs x2))) = Seg n by FINSEQ_1:def_3;
then  Sum (mlt ((abs x1),(abs x2))) <= sqrt ((Sum (sqr (abs x1))) * (Sum (sqr (abs x2)))) by A10, A9, RVSUM_1:84, SQUARE_1:22;
then  2 * (Sum (mlt ((abs x1),(abs x2)))) <= 2 * (sqrt ((Sum (sqr (abs x1))) * (Sum (sqr (abs x2))))) by XREAL_1:64;
then  (Sum (sqr (abs x1))) + (2 * (Sum (mlt ((abs x1),(abs x2))))) <= (Sum (sqr (abs x1))) + (2 * (sqrt ((Sum (sqr (abs x1))) * (Sum (sqr (abs x2)))))) by XREAL_1:7;
then A12: ((Sum (sqr (abs x1))) + (2 * (Sum (mlt ((abs x1),(abs x2)))))) + (Sum (sqr (abs x2))) <= ((Sum (sqr (abs x1))) + (2 * (sqrt ((Sum (sqr (abs x1))) * (Sum (sqr (abs x2))))))) + (Sum (sqr (abs x2))) by XREAL_1:7;
A13: 0 <= Sum (sqr (abs x2)) by RVSUM_1:86;
then A14: 0 <= sqrt (Sum (sqr (abs x2))) by SQUARE_1:def_2;
Sum (sqr ((abs x1) + (abs x2))) = Sum (((sqr (abs x1)) + (2 * (mlt ((abs x1),(abs x2))))) + (sqr (abs x2))) by RVSUM_1:68
.= (Sum ((sqr (abs x1)) + (2 * (mlt ((abs x1),(abs x2)))))) + (Sum (sqr (abs x2))) by RVSUM_1:89
.= ((Sum (sqr (abs x1))) + (Sum (2 * (mlt ((abs x1),(abs x2)))))) + (Sum (sqr (abs x2))) by RVSUM_1:89
.= ((Sum (sqr (abs x1))) + (2 * (Sum (mlt ((abs x1),(abs x2)))))) + (Sum (sqr (abs x2))) by RVSUM_1:87 ;
then  Sum (sqr (abs (x1 + x2))) <= ((Sum (sqr (abs x1))) + (2 * (Sum (mlt ((abs x1),(abs x2)))))) + (Sum (sqr (abs x2))) by A4, RVSUM_1:82;
then  Sum (sqr (x1 + x2)) <= ((Sum (sqr (abs x1))) + (2 * (Sum (mlt ((abs x1),(abs x2)))))) + (Sum (sqr (abs x2))) by Lm2;
then  Sum (sqr (x1 + x2)) <= ((Sum (sqr (abs x1))) + (2 * (sqrt ((Sum (sqr (abs x1))) * (Sum (sqr (abs x2))))))) + (Sum (sqr (abs x2))) by A12, XXREAL_0:2;
then A15: Sum (sqr (x1 + x2)) <= ((Sum (sqr (abs x1))) + (2 * ((sqrt (Sum (sqr (abs x1)))) * (sqrt (Sum (sqr (abs x2))))))) + (Sum (sqr (abs x2))) by A2, A13, SQUARE_1:29;
A16: (sqrt (Sum (sqr (abs x2)))) ^2 = Sum (sqr (abs x2)) by A13, SQUARE_1:def_2;
 Sum (sqr (abs x1)) = (sqrt (Sum (sqr (abs x1)))) ^2 by A2, SQUARE_1:def_2;
then  sqrt (Sum (sqr (x1 + x2))) <= sqrt (((sqrt (Sum (sqr (abs x1)))) + (sqrt (Sum (sqr (abs x2))))) ^2) by A15, A16, A1, SQUARE_1:26;
then  sqrt (Sum (sqr (x1 + x2))) <= (sqrt (Sum (sqr (abs x1)))) + (sqrt (Sum (sqr (abs x2)))) by A3, A14, SQUARE_1:22;
then  sqrt (Sum (sqr (x1 + x2))) <= (sqrt (Sum (sqr (abs x1)))) + (sqrt (Sum (sqr x2))) by Lm2;
hence  |.(x1 + x2).| <= |.x1.| + |.x2.| by Lm2; ::_thesis: verum
end;

theorem Th13: :: EUCLID:13
for n being Nat
for x1, x2 being Element of REAL n holds |.(x1 - x2).| <= |.x1.| + |.x2.|
proof
let n be Nat; ::_thesis: for x1, x2 being Element of REAL n holds |.(x1 - x2).| <= |.x1.| + |.x2.|
let x1, x2 be Element of REAL n; ::_thesis: |.(x1 - x2).| <= |.x1.| + |.x2.|
 |.(x1 - x2).| <= |.x1.| + |.(- x2).| by Th12;
hence  |.(x1 - x2).| <= |.x1.| + |.x2.| by Th10; ::_thesis: verum
end;

theorem :: EUCLID:14
for n being Nat
for x1, x2 being Element of REAL n holds |.x1.| - |.x2.| <= |.(x1 + x2).|
proof
let n be Nat; ::_thesis: for x1, x2 being Element of REAL n holds |.x1.| - |.x2.| <= |.(x1 + x2).|
let x1, x2 be Element of REAL n; ::_thesis: |.x1.| - |.x2.| <= |.(x1 + x2).|
reconsider R1 = x1, R2 = x2 as Element of n -tuples_on REAL ;
 x1 = (R1 + R2) - R2 by RVSUM_1:42;
then  |.x1.| <= |.(x1 + x2).| + |.x2.| by Th13;
hence  |.x1.| - |.x2.| <= |.(x1 + x2).| by XREAL_1:20; ::_thesis: verum
end;

theorem :: EUCLID:15
for n being Nat
for x1, x2 being Element of REAL n holds |.x1.| - |.x2.| <= |.(x1 - x2).|
proof
let n be Nat; ::_thesis: for x1, x2 being Element of REAL n holds |.x1.| - |.x2.| <= |.(x1 - x2).|
let x1, x2 be Element of REAL n; ::_thesis: |.x1.| - |.x2.| <= |.(x1 - x2).|
reconsider R1 = x1, R2 = x2 as Element of n -tuples_on REAL ;
 x1 = (R1 - R2) + R2 by RVSUM_1:43;
then  |.x1.| <= |.(x1 - x2).| + |.x2.| by Th12;
hence  |.x1.| - |.x2.| <= |.(x1 - x2).| by XREAL_1:20; ::_thesis: verum
end;

theorem Th16: :: EUCLID:16
for n being Nat
for x1, x2 being Element of REAL n holds
( |.(x1 - x2).| = 0 iff x1 = x2 )
proof
let n be Nat; ::_thesis: for x1, x2 being Element of REAL n holds
( |.(x1 - x2).| = 0 iff x1 = x2 )
let x1, x2 be Element of REAL n; ::_thesis: ( |.(x1 - x2).| = 0 iff x1 = x2 )
reconsider R1 = x1, R2 = x2 as Element of n -tuples_on REAL ;
thus  ( |.(x1 - x2).| = 0 implies x1 = x2 ) ::_thesis: ( x1 = x2 implies |.(x1 - x2).| = 0 )
proof
assume  |.(x1 - x2).| = 0 ; ::_thesis: x1 = x2
then R1 - R2 = 0* n by Th8
.= n |-> 0 ;
hence  x1 = x2 by RVSUM_1:38; ::_thesis: verum
end;
assume  x1 = x2 ; ::_thesis: |.(x1 - x2).| = 0
then  R1 - R2 = 0* n by RVSUM_1:37;
hence  |.(x1 - x2).| = 0 by Th7; ::_thesis: verum
end;

registration
let n be Nat;
let x1 be Element of REAL n;
cluster|.(x1 - x1).| ->  zero ;
coherence
 |.(x1 - x1).| is empty by Th16;
end;

theorem :: EUCLID:17
for n being Nat
for x1, x2 being Element of REAL n st x1 <> x2 holds
|.(x1 - x2).| > 0
proof
let n be Nat; ::_thesis: for x1, x2 being Element of REAL n st x1 <> x2 holds
|.(x1 - x2).| > 0
let x1, x2 be Element of REAL n; ::_thesis: ( x1 <> x2 implies |.(x1 - x2).| > 0 )
assume  x1 <> x2 ; ::_thesis: |.(x1 - x2).| > 0
then  0 <> |.(x1 - x2).| by Th16;
hence  |.(x1 - x2).| > 0 ; ::_thesis: verum
end;

theorem Th18: :: EUCLID:18
for n being Nat
for x1, x2 being Element of REAL n holds |.(x1 - x2).| = |.(x2 - x1).|
proof
let n be Nat; ::_thesis: for x1, x2 being Element of REAL n holds |.(x1 - x2).| = |.(x2 - x1).|
let x1, x2 be Element of REAL n; ::_thesis: |.(x1 - x2).| = |.(x2 - x1).|
reconsider R1 = x1, R2 = x2 as Element of n -tuples_on REAL ;
thus |.(x1 - x2).| = |.(- (R2 - R1)).| by RVSUM_1:35
.= |.(x2 - x1).| by Th10 ; ::_thesis: verum
end;

theorem Th19: :: EUCLID:19
for n being Nat
for x1, x2, x being Element of REAL n holds |.(x1 - x2).| <= |.(x1 - x).| + |.(x - x2).|
proof
let n be Nat; ::_thesis: for x1, x2, x being Element of REAL n holds |.(x1 - x2).| <= |.(x1 - x).| + |.(x - x2).|
let x1, x2, x be Element of REAL n; ::_thesis: |.(x1 - x2).| <= |.(x1 - x).| + |.(x - x2).|
reconsider R1 = x1, R2 = x2, R = x as Element of n -tuples_on REAL ;
|.(x1 - x2).| = |.(((R1 - R) + R) - R2).| by RVSUM_1:43
.= |.((x1 - x) + (x - x2)).| by RVSUM_1:40 ;
hence  |.(x1 - x2).| <= |.(x1 - x).| + |.(x - x2).| by Th12; ::_thesis: verum
end;

definition
let n be Nat;
func Pitag_dist n ->  Function of [:(REAL n),(REAL n):],REAL means :Def6: :: EUCLID:def 6
 for x, y being Element of REAL n holds it . (x,y) = |.(x - y).|;
existence
 ex b1 being Function of [:(REAL n),(REAL n):],REAL st
for x, y being Element of REAL n holds b1 . (x,y) = |.(x - y).|
proof
deffunc H1( Element of REAL n, Element of REAL n) ->  Real = |.($1 - $2).|;
consider f being Function of [:(REAL n),(REAL n):],REAL such that
A1: for x, y being Element of REAL n holds f . (x,y) = H1(x,y) from BINOP_1:sch_4();
take  f ; ::_thesis: for x, y being Element of REAL n holds f . (x,y) = |.(x - y).|
let x, y be Element of REAL n; ::_thesis: f . (x,y) = |.(x - y).|
thus  f . (x,y) = |.(x - y).| by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:(REAL n),(REAL n):],REAL st ( for x, y being Element of REAL n holds b1 . (x,y) = |.(x - y).| ) & ( for x, y being Element of REAL n holds b2 . (x,y) = |.(x - y).| ) holds
b1 = b2
proof
let f, g be Function of [:(REAL n),(REAL n):],REAL; ::_thesis: ( ( for x, y being Element of REAL n holds f . (x,y) = |.(x - y).| ) & ( for x, y being Element of REAL n holds g . (x,y) = |.(x - y).| ) implies f = g )
assume that
A2: for x, y being Element of REAL n holds f . (x,y) = |.(x - y).| and
A3: for x, y being Element of REAL n holds g . (x,y) = |.(x - y).| ; ::_thesis: f = g
reconsider n = n as Element of NAT by ORDINAL1:def_12;
reconsider f = f, g = g as Function of [:(REAL n),(REAL n):],REAL ;
now__::_thesis:_for_x,_y_being_Element_of_REAL_n_holds_f_._(x,y)_=_g_._(x,y)
let x, y be Element of REAL n; ::_thesis: f . (x,y) = g . (x,y)
thus f . (x,y) = |.(x - y).| by A2
.= g . (x,y) by A3 ; ::_thesis: verum
end;
hence  f = g by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines Pitag_dist EUCLID:def_6_:_
 for n being Nat
for b2 being Function of [:(REAL n),(REAL n):],REAL holds
( b2 = Pitag_dist n iff for x, y being Element of REAL n holds b2 . (x,y) = |.(x - y).| );

theorem :: EUCLID:20
for x, y being real-valued FinSequence holds sqr (x - y) = sqr (y - x)
proof
let x, y be real-valued FinSequence; ::_thesis: sqr (x - y) = sqr (y - x)
thus (x - y) ^2 = ((x ^2) - (2 (#) (x (#) y))) + (y ^2) by RVSUM_1:69
.= (sqr y) + ((- (2 * (mlt (x,y)))) + (sqr x))
.= ((sqr y) - (2 * (mlt (y,x)))) + (sqr x) by RFUNCT_1:8
.= sqr (y - x) by RVSUM_1:69 ; ::_thesis: verum
end;

theorem Th21: :: EUCLID:21
for n being Nat holds Pitag_dist n is_metric_of REAL n
proof
let n be Nat; ::_thesis: Pitag_dist n is_metric_of REAL n
let x, y, z be Element of REAL n; :: according to PCOMPS_1:def_6 ::_thesis: ( ( not (Pitag_dist n) . (x,y) = 0 or x = y ) & ( not x = y or (Pitag_dist n) . (x,y) = 0 ) & (Pitag_dist n) . (x,y) = (Pitag_dist n) . (y,x) & (Pitag_dist n) . (x,z) <= ((Pitag_dist n) . (x,y)) + ((Pitag_dist n) . (y,z)) )
A1: (Pitag_dist n) . (y,z) = |.(y - z).| by Def6;
 (Pitag_dist n) . (x,y) = |.(x - y).| by Def6;
hence  ( (Pitag_dist n) . (x,y) = 0 iff x = y ) by Th16; ::_thesis: ( (Pitag_dist n) . (x,y) = (Pitag_dist n) . (y,x) & (Pitag_dist n) . (x,z) <= ((Pitag_dist n) . (x,y)) + ((Pitag_dist n) . (y,z)) )
thus (Pitag_dist n) . (x,y) = |.(x - y).| by Def6
.= |.(y - x).| by Th18
.= (Pitag_dist n) . (y,x) by Def6 ; ::_thesis: (Pitag_dist n) . (x,z) <= ((Pitag_dist n) . (x,y)) + ((Pitag_dist n) . (y,z))
 ( (Pitag_dist n) . (x,y) = |.(x - y).| & (Pitag_dist n) . (x,z) = |.(x - z).| ) by Def6;
hence  (Pitag_dist n) . (x,z) <= ((Pitag_dist n) . (x,y)) + ((Pitag_dist n) . (y,z)) by A1, Th19; ::_thesis: verum
end;

definition
let n be Nat;
func Euclid n ->  strict MetrSpace equals :: EUCLID:def 7
 MetrStruct(# (REAL n),(Pitag_dist n) #);
coherence
 MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrSpace
proof
 SpaceMetr ((REAL n),(Pitag_dist n)) = MetrStruct(# (REAL n),(Pitag_dist n) #) by Th21, PCOMPS_1:def_7;
hence  MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrSpace ; ::_thesis: verum
end;
end;

:: deftheorem  defines Euclid EUCLID:def_7_:_
 for n being Nat holds Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #);

registration
let n be Nat;
cluster Euclid n ->  non empty strict ;
coherence
 not Euclid n is empty ;
end;

definition
let n be Nat;
func TOP-REAL n ->  strict RLTopStruct  means :Def8: :: EUCLID:def 8
( TopStruct(# the carrier of it, the topology of it #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of it, the ZeroF of it, the addF of it, the Mult of it #) = RealVectSpace (Seg n) );
existence
 ex b1 being strict RLTopStruct st
( TopStruct(# the carrier of b1, the topology of b1 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = RealVectSpace (Seg n) )
proof
set V = RealVectSpace (Seg n);
set T = TopSpaceMetr (Euclid n);
reconsider t = the topology of (TopSpaceMetr (Euclid n)) as Subset-Family of the carrier of (RealVectSpace (Seg n)) by FINSEQ_2:93;
take S = RLTopStruct(# the carrier of (RealVectSpace (Seg n)), the ZeroF of (RealVectSpace (Seg n)), the addF of (RealVectSpace (Seg n)), the Mult of (RealVectSpace (Seg n)),t #); ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of S, the ZeroF of S, the addF of S, the Mult of S #) = RealVectSpace (Seg n) )
thus  TopStruct(# the carrier of S, the topology of S #) = TopSpaceMetr (Euclid n) by FINSEQ_2:93; ::_thesis: RLSStruct(# the carrier of S, the ZeroF of S, the addF of S, the Mult of S #) = RealVectSpace (Seg n)
thus  RLSStruct(# the carrier of S, the ZeroF of S, the addF of S, the Mult of S #) = RealVectSpace (Seg n) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict RLTopStruct st TopStruct(# the carrier of b1, the topology of b1 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = RealVectSpace (Seg n) & TopStruct(# the carrier of b2, the topology of b2 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = RealVectSpace (Seg n) holds
b1 = b2 ;
end;

:: deftheorem Def8 defines TOP-REAL EUCLID:def_8_:_
 for n being Nat
for b2 being strict RLTopStruct holds
( b2 = TOP-REAL n iff ( TopStruct(# the carrier of b2, the topology of b2 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = RealVectSpace (Seg n) ) );

registration
let n be Nat;
cluster TOP-REAL n ->  non empty strict ;
coherence
 not TOP-REAL n is empty
proof
 TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by Def8;
hence  not TOP-REAL n is empty ; ::_thesis: verum
end;
end;

registration
let n be Nat;
cluster TOP-REAL n ->  TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ;
coherence
 ( TOP-REAL n is TopSpace-like & TOP-REAL n is Abelian & TOP-REAL n is add-associative & TOP-REAL n is right_zeroed & TOP-REAL n is right_complementable & TOP-REAL n is vector-distributive & TOP-REAL n is scalar-distributive & TOP-REAL n is scalar-associative & TOP-REAL n is scalar-unital )
proof
 TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by Def8;
hence  TOP-REAL n is TopSpace-like by PRE_TOPC:28; ::_thesis: ( TOP-REAL n is Abelian & TOP-REAL n is add-associative & TOP-REAL n is right_zeroed & TOP-REAL n is right_complementable & TOP-REAL n is vector-distributive & TOP-REAL n is scalar-distributive & TOP-REAL n is scalar-associative & TOP-REAL n is scalar-unital )
 RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) = RealVectSpace (Seg n) by Def8;
hence  ( TOP-REAL n is Abelian & TOP-REAL n is add-associative & TOP-REAL n is right_zeroed & TOP-REAL n is right_complementable & TOP-REAL n is vector-distributive & TOP-REAL n is scalar-distributive & TOP-REAL n is scalar-associative & TOP-REAL n is scalar-unital ) by RSSPACE:15; ::_thesis: verum
end;
end;


theorem Th22: :: EUCLID:22
for n being Nat holds the carrier of (TOP-REAL n) = REAL n
proof
let n be Nat; ::_thesis: the carrier of (TOP-REAL n) = REAL n
 TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by Def8;
hence  the carrier of (TOP-REAL n) = REAL n ; ::_thesis: verum
end;

theorem Th23: :: EUCLID:23
for n being Nat
for p being Point of (TOP-REAL n) holds p is Function of (Seg n),REAL
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds p is Function of (Seg n),REAL
let p be Point of (TOP-REAL n); ::_thesis: p is Function of (Seg n),REAL
 TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by Def8;
then  p is Element of Funcs ((Seg n),REAL) by FINSEQ_2:93;
hence  p is Function of (Seg n),REAL ; ::_thesis: verum
end;

theorem Th24: :: EUCLID:24
for n being Nat
for p being Point of (TOP-REAL n) holds p is FinSequence of REAL
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds p is FinSequence of REAL
let p be Point of (TOP-REAL n); ::_thesis: p is FinSequence of REAL
 p is Function of (Seg n),REAL by Th23;
hence  p is FinSequence of REAL by FINSEQ_2:25; ::_thesis: verum
end;

registration
let n be Nat;
cluster TOP-REAL n ->  constituted-FinSeqs strict ;
coherence
 TOP-REAL n is constituted-FinSeqs
proof
let a be Element of (TOP-REAL n); :: according to MONOID_0:def_2 ::_thesis: a is set
thus  a is set by Th24; ::_thesis: verum
end;
end;

registration
let n be Nat;
cluster  ->  FinSequence-like for Element of the carrier of (TOP-REAL n);
coherence
 for b1 being Point of (TOP-REAL n) holds b1 is FinSequence-like ;
end;

registration
let n be Nat;
cluster  ->  real-valued for Element of the carrier of (TOP-REAL n);
coherence
 for b1 being Point of (TOP-REAL n) holds b1 is real-valued by Th24;
end;

Lm3:  for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds
p1 + p2 = r1 + r2
proof
let n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds
p1 + p2 = r1 + r2
let p1, p2 be Point of (TOP-REAL n); ::_thesis: for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds
p1 + p2 = r1 + r2
A1: REAL n = Funcs ((Seg n),REAL) by FINSEQ_2:93;
let r1, r2 be real-valued Function; ::_thesis: ( p1 = r1 & p2 = r2 implies p1 + p2 = r1 + r2 )
assume A2: ( p1 = r1 & p2 = r2 ) ; ::_thesis: p1 + p2 = r1 + r2
reconsider s1 = r1, s2 = r2 as Element of REAL n by A2, Th22;
 RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) = RealVectSpace (Seg n) by Def8;
hence p1 + p2 = (RealFuncAdd (Seg n)) . (r1,r2) by A2, ALGSTR_0:def_1
.= s1 + s2 by A1, FUNCSDOM:def_1
.= r1 + r2 ;
::_thesis: verum
end;

Lm4:  for n being Nat
for p being Point of (TOP-REAL n)
for x being real number
for r being real-valued Function st p = r holds
x * p = x (#) r
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n)
for x being real number
for r being real-valued Function st p = r holds
x * p = x (#) r
let p be Point of (TOP-REAL n); ::_thesis: for x being real number
for r being real-valued Function st p = r holds
x * p = x (#) r
let x be real number ; ::_thesis: for r being real-valued Function st p = r holds
x * p = x (#) r
reconsider x1 = x as Real by XREAL_0:def_1;
let r be real-valued Function; ::_thesis: ( p = r implies x * p = x (#) r )
assume A1: p = r ; ::_thesis: x * p = x (#) r
reconsider s = r as Element of REAL n by A1, Th22;
 REAL n = Funcs ((Seg n),REAL) by FINSEQ_2:93;
then reconsider f = s as Function of (Seg n),REAL by FUNCT_2:66;
 RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) = RealVectSpace (Seg n) by Def8;
hence x * p = multreal [;] (x1,f) by A1, FUNCSDOM:def_3
.= multreal [;] (x,((id REAL) * f)) by PARTFUN1:7
.= x * s by FUNCOP_1:34
.= x (#) r ;
::_thesis: verum
end;

registration
let r, s be real number ;
let n be Nat;
let p be Element of (TOP-REAL n);
let f be real-valued FinSequence;
identifyr * p with s * f when r = s, p = f;
compatibility
 ( r = s & p = f implies r * p = s * f ) by Lm4;
end;

registration
let n be Nat;
let p, q be Element of (TOP-REAL n);
let f, g be real-valued FinSequence;
identifyp + q with f + g when p = f, q = g;
compatibility
 ( p = f & q = g implies p + q = f + g ) by Lm3;
end;

registration
let n be Nat;
let p be Element of (TOP-REAL n);
let f be real-valued FinSequence;
identify - p with  - f when p = f;
compatibility
 ( p = f implies - p = - f )
proof
assume A1: p = f ; ::_thesis: - p = - f
thus  - p = (- 1) * p by RLVECT_1:16
.= - f by A1 ; ::_thesis: verum
end;
end;

registration
let n be Nat;
let p, q be Element of (TOP-REAL n);
let f, g be real-valued FinSequence;
identifyp - q with f - g when p = f, q = g;
compatibility
 ( p = f & q = g implies p - q = f - g ) ;
end;

registration
let n be Nat;
cluster  -> n -element for Element of the carrier of (TOP-REAL n);
coherence
 for b1 being Point of (TOP-REAL n) holds b1 is n -element
proof
let p be Point of (TOP-REAL n); ::_thesis: p is n -element
A1: p is Function of (Seg n),REAL by Th23;
Seg (len p) = dom p by FINSEQ_1:def_3
.= Seg n by A1, FUNCT_2:def_1 ;
hence  len p = n by FINSEQ_1:6; :: according to CARD_1:def_7 ::_thesis: verum
end;
end;

notation
let n be Nat;
synonym  0.REAL n for  0* n;
end;

definition
let n be Nat;
:: original: 0*
redefine func 0.REAL n ->  Point of (TOP-REAL n);
coherence
 0* n is Point of (TOP-REAL n)
proof
 TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by Def8;
hence  0* n is Point of (TOP-REAL n) ; ::_thesis: verum
end;
end;

theorem :: EUCLID:25
for n being Nat
for x being Element of REAL n holds sqr (abs x) = sqr x by Lm2;

theorem :: EUCLID:26
for n being Nat
for p1, p2, p3 being Point of (TOP-REAL n) holds (p1 + p2) + p3 = p1 + (p2 + p3) by RLVECT_1:def_3;

theorem :: EUCLID:27
for n being Nat
for p being Point of (TOP-REAL n) holds
( (0. (TOP-REAL n)) + p = p & p + (0. (TOP-REAL n)) = p ) by RLVECT_1:4;

theorem :: EUCLID:28
for n being Nat
for x being real number holds x * (0. (TOP-REAL n)) = 0. (TOP-REAL n) by RLVECT_1:10;

theorem :: EUCLID:29
for n being Nat
for p being Point of (TOP-REAL n) holds
( 1 * p = p & 0 * p = 0. (TOP-REAL n) ) by RLVECT_1:10, RLVECT_1:def_8;

theorem :: EUCLID:30
for n being Nat
for p being Point of (TOP-REAL n)
for x, y being real number holds (x * y) * p = x * (y * p) by RLVECT_1:def_7;

theorem :: EUCLID:31
for n being Nat
for p being Point of (TOP-REAL n)
for x being real number holds
( not x * p = 0. (TOP-REAL n) or x = 0 or p = 0. (TOP-REAL n) ) by RLVECT_1:11;

theorem :: EUCLID:32
for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for x being real number holds x * (p1 + p2) = (x * p1) + (x * p2) by RLVECT_1:def_5;

theorem :: EUCLID:33
for n being Nat
for p being Point of (TOP-REAL n)
for x, y being real number holds (x + y) * p = (x * p) + (y * p) by RLVECT_1:def_6;

theorem :: EUCLID:34
for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for x being real number holds
( not x * p1 = x * p2 or x = 0 or p1 = p2 ) by RLVECT_1:36;

theorem :: EUCLID:35
canceled;

theorem :: EUCLID:36
for n being Nat
for p being Point of (TOP-REAL n) holds p + (- p) = 0. (TOP-REAL n) by RLVECT_1:5;

theorem :: EUCLID:37
for n being Nat
for p1, p2 being Point of (TOP-REAL n) st p1 + p2 = 0. (TOP-REAL n) holds
p1 = - p2 by RLVECT_1:6;

theorem :: EUCLID:38
for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds - (p1 + p2) = (- p1) - p2 by RLVECT_1:30;

theorem :: EUCLID:39
for n being Nat
for p being Point of (TOP-REAL n) holds - p = (- 1) * p ;

theorem :: EUCLID:40
for n being Nat
for p being Point of (TOP-REAL n)
for x being real number holds
( - (x * p) = (- x) * p & - (x * p) = x * (- p) ) by RLVECT_1:25, RLVECT_1:79;

theorem :: EUCLID:41
for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds p1 - p2 = p1 + (- p2) ;

theorem :: EUCLID:42
for n being Nat
for p being Point of (TOP-REAL n) holds p - p = 0. (TOP-REAL n) by RLVECT_1:5;

theorem :: EUCLID:43
for n being Nat
for p1, p2 being Point of (TOP-REAL n) st p1 - p2 = 0. (TOP-REAL n) holds
p1 = p2 by RLVECT_1:21;

theorem :: EUCLID:44
for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds
( - (p1 - p2) = p2 - p1 & - (p1 - p2) = (- p1) + p2 ) by RLVECT_1:33;

theorem :: EUCLID:45
for n being Nat
for p1, p2, p3 being Point of (TOP-REAL n) holds p1 + (p2 - p3) = (p1 + p2) - p3 by RLVECT_1:def_3;

theorem :: EUCLID:46
for n being Nat
for p1, p2, p3 being Point of (TOP-REAL n) holds p1 - (p2 + p3) = (p1 - p2) - p3 by RLVECT_1:27;

theorem :: EUCLID:47
for n being Nat
for p1, p2, p3 being Point of (TOP-REAL n) holds p1 - (p2 - p3) = (p1 - p2) + p3 by RLVECT_1:29;

theorem :: EUCLID:48
for n being Nat
for p, p1 being Point of (TOP-REAL n) holds
( p = (p + p1) - p1 & p = (p - p1) + p1 ) by RLVECT_4:1;

theorem :: EUCLID:49
for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for x being real number holds x * (p1 - p2) = (x * p1) - (x * p2) by RLVECT_1:34;

theorem :: EUCLID:50
for n being Nat
for p being Point of (TOP-REAL n)
for x, y being real number holds (x - y) * p = (x * p) - (y * p) by RLVECT_1:35;


theorem :: EUCLID:51
for p being Point of (TOP-REAL 2) ex x, y being Real st p = <*x,y*>
proof
let p be Point of (TOP-REAL 2); ::_thesis: ex x, y being Real st p = <*x,y*>
 TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by Def8;
then  p is Tuple of 2, REAL by FINSEQ_2:131;
hence  ex x, y being Real st p = <*x,y*> by FINSEQ_2:100; ::_thesis: verum
end;

definition
let p be Point of (TOP-REAL 2);
funcp `1  ->  Real equals :: EUCLID:def 9
p . 1;
coherence
 p . 1 is Real ;
funcp `2  ->  Real equals :: EUCLID:def 10
p . 2;
coherence
 p . 2 is Real ;
end;

:: deftheorem  defines `1 EUCLID:def_9_:_
 for p being Point of (TOP-REAL 2) holds p `1 = p . 1;

:: deftheorem  defines `2 EUCLID:def_10_:_
 for p being Point of (TOP-REAL 2) holds p `2 = p . 2;

notation
let x, y be real number ;
synonym |[x,y]| for <*x,y*>;
end;

definition
let x, y be real number ;
:: original: |[
redefine func|[x,y]| ->  Point of (TOP-REAL 2);
coherence
 |[x,y]| is Point of (TOP-REAL 2)
proof
A1: y is Real by XREAL_0:def_1;
 ( TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) & x is Real ) by Def8, XREAL_0:def_1;
hence  |[x,y]| is Point of (TOP-REAL 2) by A1, FINSEQ_2:101; ::_thesis: verum
end;
end;

theorem :: EUCLID:52
for x, y being real number holds
( |[x,y]| `1 = x & |[x,y]| `2 = y ) by FINSEQ_1:44;

theorem Th53: :: EUCLID:53
for p being Point of (TOP-REAL 2) holds p = |[(p `1),(p `2)]|
proof
let p be Point of (TOP-REAL 2); ::_thesis: p = |[(p `1),(p `2)]|
 TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by Def8;
then  p is Tuple of 2, REAL by FINSEQ_2:131;
then consider x, y being Real such that
A1: p = <*x,y*> by FINSEQ_2:100;
 p `1 = x by A1, FINSEQ_1:44;
hence  p = |[(p `1),(p `2)]| by A1, FINSEQ_1:44; ::_thesis: verum
end;

theorem :: EUCLID:54
0. (TOP-REAL 2) = |[0,0]|
proof
 ( RLSStruct(# the carrier of (TOP-REAL 2), the ZeroF of (TOP-REAL 2), the addF of (TOP-REAL 2), the Mult of (TOP-REAL 2) #) = RealVectSpace (Seg 2) & 0.REAL 2 = |[0,0]| ) by Def8, FINSEQ_2:61;
hence  0. (TOP-REAL 2) = |[0,0]| ; ::_thesis: verum
end;

theorem Th55: :: EUCLID:55
for p1, p2 being Point of (TOP-REAL 2) holds p1 + p2 = |[((p1 `1) + (p2 `1)),((p1 `2) + (p2 `2))]|
proof
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: p1 + p2 = |[((p1 `1) + (p2 `1)),((p1 `2) + (p2 `2))]|
 TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by Def8;
then reconsider p19 = p1, p29 = p2 as Element of REAL 2 ;
 len (p19 + p29) = 2 by CARD_1:def_7;
then A1: dom (p19 + p29) = Seg 2 by FINSEQ_1:def_3;
 2 in {1,2} by TARSKI:def_2;
then A2: (p1 + p2) `2 = (p1 `2) + (p2 `2) by A1, FINSEQ_1:2, VALUED_1:def_1;
 1 in {1,2} by TARSKI:def_2;
then  (p1 + p2) `1 = (p1 `1) + (p2 `1) by A1, FINSEQ_1:2, VALUED_1:def_1;
hence  p1 + p2 = |[((p1 `1) + (p2 `1)),((p1 `2) + (p2 `2))]| by A2, Th53; ::_thesis: verum
end;

theorem :: EUCLID:56
for x1, y1, x2, y2 being real number holds |[x1,y1]| + |[x2,y2]| = |[(x1 + x2),(y1 + y2)]|
proof
let x1, y1, x2, y2 be real number ; ::_thesis: |[x1,y1]| + |[x2,y2]| = |[(x1 + x2),(y1 + y2)]|
A1: ( |[x2,y2]| `1 = x2 & |[x2,y2]| `2 = y2 ) by FINSEQ_1:44;
 ( |[x1,y1]| `1 = x1 & |[x1,y1]| `2 = y1 ) by FINSEQ_1:44;
hence  |[x1,y1]| + |[x2,y2]| = |[(x1 + x2),(y1 + y2)]| by A1, Th55; ::_thesis: verum
end;

theorem Th57: :: EUCLID:57
for x being real number
for p being Point of (TOP-REAL 2) holds x * p = |[(x * (p `1)),(x * (p `2))]|
proof
let x be real number ; ::_thesis: for p being Point of (TOP-REAL 2) holds x * p = |[(x * (p `1)),(x * (p `2))]|
let p be Point of (TOP-REAL 2); ::_thesis: x * p = |[(x * (p `1)),(x * (p `2))]|
 ( (x * p) `1 = x * (p `1) & (x * p) `2 = x * (p `2) ) by RVSUM_1:44;
hence  x * p = |[(x * (p `1)),(x * (p `2))]| by Th53; ::_thesis: verum
end;

theorem :: EUCLID:58
for x, x1, y1 being real number holds x * |[x1,y1]| = |[(x * x1),(x * y1)]|
proof
let x, x1, y1 be real number ; ::_thesis: x * |[x1,y1]| = |[(x * x1),(x * y1)]|
 ( |[x1,y1]| `1 = x1 & |[x1,y1]| `2 = y1 ) by FINSEQ_1:44;
hence  x * |[x1,y1]| = |[(x * x1),(x * y1)]| by Th57; ::_thesis: verum
end;

theorem Th59: :: EUCLID:59
for p being Point of (TOP-REAL 2) holds - p = |[(- (p `1)),(- (p `2))]|
proof
let p be Point of (TOP-REAL 2); ::_thesis: - p = |[(- (p `1)),(- (p `2))]|
thus  - p = (- 1) * p
.= |[((- 1) * (p `1)),((- 1) * (p `2))]| by Th57
.= |[(- (p `1)),(- (p `2))]| ; ::_thesis: verum
end;

theorem :: EUCLID:60
for x1, y1 being real number holds - |[x1,y1]| = |[(- x1),(- y1)]|
proof
let x1, y1 be real number ; ::_thesis: - |[x1,y1]| = |[(- x1),(- y1)]|
 ( |[x1,y1]| `1 = x1 & |[x1,y1]| `2 = y1 ) by FINSEQ_1:44;
hence  - |[x1,y1]| = |[(- x1),(- y1)]| by Th59; ::_thesis: verum
end;

theorem Th61: :: EUCLID:61
for p1, p2 being Point of (TOP-REAL 2) holds p1 - p2 = |[((p1 `1) - (p2 `1)),((p1 `2) - (p2 `2))]|
proof
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: p1 - p2 = |[((p1 `1) - (p2 `1)),((p1 `2) - (p2 `2))]|
 - p2 = |[(- (p2 `1)),(- (p2 `2))]| by Th59;
then  ( (- p2) `1 = - (p2 `1) & (- p2) `2 = - (p2 `2) ) by FINSEQ_1:44;
hence p1 - p2 = |[((p1 `1) + (- (p2 `1))),((p1 `2) + (- (p2 `2)))]| by Th55
.= |[((p1 `1) - (p2 `1)),((p1 `2) - (p2 `2))]| ;
::_thesis: verum
end;

theorem :: EUCLID:62
for x1, y1, x2, y2 being real number holds |[x1,y1]| - |[x2,y2]| = |[(x1 - x2),(y1 - y2)]|
proof
let x1, y1, x2, y2 be real number ; ::_thesis: |[x1,y1]| - |[x2,y2]| = |[(x1 - x2),(y1 - y2)]|
A1: ( |[x2,y2]| `1 = x2 & |[x2,y2]| `2 = y2 ) by FINSEQ_1:44;
 ( |[x1,y1]| `1 = x1 & |[x1,y1]| `2 = y1 ) by FINSEQ_1:44;
hence  |[x1,y1]| - |[x2,y2]| = |[(x1 - x2),(y1 - y2)]| by A1, Th61; ::_thesis: verum
end;

theorem :: EUCLID:63
for n being Nat
for P being Subset of (TOP-REAL n)
for Q being non empty Subset of (Euclid n) st P = Q holds
(TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q)
proof
let n be Nat; ::_thesis: for P being Subset of (TOP-REAL n)
for Q being non empty Subset of (Euclid n) st P = Q holds
(TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q)
let P be Subset of (TOP-REAL n); ::_thesis: for Q being non empty Subset of (Euclid n) st P = Q holds
(TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q)
let Q be non empty Subset of (Euclid n); ::_thesis: ( P = Q implies (TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q) )
set M = TopSpaceMetr ((Euclid n) | Q);
 TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by Def8;
then  TopSpaceMetr ((Euclid n) | Q) is SubSpace of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TOPMETR:13;
then reconsider M = TopSpaceMetr ((Euclid n) | Q) as SubSpace of TOP-REAL n by PRE_TOPC:29;
assume  P = Q ; ::_thesis: (TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q)
then  [#] M = P by TOPMETR:def_2;
hence  (TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q) by PRE_TOPC:def_5; ::_thesis: verum
end;

theorem :: EUCLID:64
for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds
p1 + p2 = r1 + r2 ;

theorem :: EUCLID:65
for n being Nat
for x being real number
for p being Point of (TOP-REAL n)
for r being real-valued Function st p = r holds
x * p = x (#) r ;

theorem Th66: :: EUCLID:66
for n being Nat holds 0.REAL n = 0. (TOP-REAL n)
proof
let n be Nat; ::_thesis: 0.REAL n = 0. (TOP-REAL n)
 RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) = RealVectSpace (Seg n) by Def8;
hence  0.REAL n = 0. (TOP-REAL n) ; ::_thesis: verum
end;

theorem Th67: :: EUCLID:67
for n being Nat holds the carrier of (Euclid n) = the carrier of (TOP-REAL n)
proof
let n be Nat; ::_thesis: the carrier of (Euclid n) = the carrier of (TOP-REAL n)
thus  the carrier of (Euclid n) = the carrier of (TopSpaceMetr (Euclid n))
.= the carrier of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by Def8
.= the carrier of (TOP-REAL n) ; ::_thesis: verum
end;

theorem :: EUCLID:68
for n being Nat
for p1 being Point of (TOP-REAL n)
for r1 being real-valued Function st p1 = r1 holds
- p1 = - r1 ;

theorem :: EUCLID:69
for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds
p1 - p2 = r1 - r2 ;

theorem :: EUCLID:70
for n being Nat holds 0. (TOP-REAL n) = 0* n by Th66;

theorem :: EUCLID:71
for n being Nat
for p being Point of (TOP-REAL n) holds |.(- p).| = |.p.| by Th10;

registration
let n be Nat;
let D be set ;
clustern -tuples_on D ->  FinSequence-membered ;
coherence
 n -tuples_on D is FinSequence-membered ;
end;

registration
let n be Nat;
cluster REAL n ->  FinSequence-membered ;
coherence
 REAL n is FinSequence-membered ;
end;

registration
let n be Nat;
cluster REAL n ->  real-functions-membered ;
coherence
 REAL n is real-functions-membered
proof
let x be set ; :: according to VALUED_2:def_4 ::_thesis: ( not x in REAL n or x is set )
assume  x in REAL n ; ::_thesis: x is set
then reconsider x = x as Element of REAL n ;
 x is real-valued ;
hence  x is set ; ::_thesis: verum
end;
end;

definition
let n be Nat;
func 1* n ->  FinSequence of REAL  equals :: EUCLID:def 11
n |-> 1;
coherence
 n |-> 1 is FinSequence of REAL ;
end;

:: deftheorem  defines 1* EUCLID:def_11_:_
 for n being Nat holds 1* n = n |-> 1;

definition
let n be Nat;
:: original: 1*
redefine func 1* n ->  Element of REAL n;
coherence
 1* n is Element of REAL n ;
end;

definition
let n be Nat;
func 1.REAL n ->  Point of (TOP-REAL n) equals :: EUCLID:def 12
 1* n;
coherence
 1* n is Point of (TOP-REAL n) by Th22;
end;

:: deftheorem  defines 1.REAL EUCLID:def_12_:_
 for n being Nat holds 1.REAL n = 1* n;

theorem :: EUCLID:72
for n being Nat holds abs (1* n) = n |-> 1
proof
let n be Nat; ::_thesis: abs (1* n) = n |-> 1
thus  abs (1* n) = n |-> (absreal . 1) by FINSEQOP:16
.= n |-> (abs 1) by Def2
.= n |-> 1 by ABSVALUE:def_1 ; ::_thesis: verum
end;

theorem Th73: :: EUCLID:73
for n being Nat holds |.(1* n).| = sqrt n
proof
let n be Nat; ::_thesis: |.(1* n).| = sqrt n
reconsider f = n |-> (1 ^2) as FinSequence of REAL ;
thus |.(1* n).| = sqrt (Sum f) by RVSUM_1:56
.= sqrt (n * 1) by RVSUM_1:80
.= sqrt n ; ::_thesis: verum
end;

theorem :: EUCLID:74
for n being Nat holds |.(1.REAL n).| = sqrt n by Th73;

theorem :: EUCLID:75
for n being Nat st 1 <= n holds
1 <= |.(1.REAL n).|
proof
let n be Nat; ::_thesis: ( 1 <= n implies 1 <= |.(1.REAL n).| )
assume A1: 1 <= n ; ::_thesis: 1 <= |.(1.REAL n).|
 |.(1.REAL n).| = sqrt n by Th73;
hence  1 <= |.(1.REAL n).| by A1, SQUARE_1:18, SQUARE_1:26; ::_thesis: verum
end;

theorem :: EUCLID:76
for f being FinSequence of REAL holds
( f is Element of REAL (len f) & f is Point of (TOP-REAL (len f)) )
proof
let f be FinSequence of REAL ; ::_thesis: ( f is Element of REAL (len f) & f is Point of (TOP-REAL (len f)) )
 f is Element of REAL * by FINSEQ_1:def_11;
then  ( the carrier of (TOP-REAL (len f)) = the carrier of (Euclid (len f)) & f in (len f) -tuples_on REAL ) by Th67;
hence  ( f is Element of REAL (len f) & f is Point of (TOP-REAL (len f)) ) ; ::_thesis: verum
end;

theorem :: EUCLID:77
REAL 0 = {(0. (TOP-REAL 0))}
proof
thus  REAL 0 = {(<*> REAL)} by FINSEQ_2:94
.= {(0. (TOP-REAL 0))} ; ::_thesis: verum
end;