:: The Euclidean Space
::  by Agata Darmochwa{\l}
::
:: Received November 21, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, NAT_1, XREAL_0, ORDINAL1, FINSEQ_2, FINSEQ_1, SUBSET_1,
      FUNCT_1, COMPLEX1, REAL_1, VALUED_0, RELAT_1, TARSKI, CARD_1, ARYTM_1,
      ARYTM_3, RVSUM_1, SQUARE_1, CARD_3, XXREAL_0, XCMPLX_0, ZFMISC_1,
      VALUED_1, PCOMPS_1, STRUCT_0, METRIC_1, XBOOLE_0, RLTOPSP1, PRE_TOPC,
      RLVECT_1, FUNCSDOM, SETFAM_1, ALGSTR_0, FUNCT_2, MONOID_0, BINOP_2,
      FUNCOP_1, SUPINF_2, MCART_1, EUCLID, VALUED_2, JORDAN2C;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
      XCMPLX_0, SETFAM_1, XREAL_0, COMPLEX1, NAT_1, RELAT_1, FUNCT_1, VALUED_0,
      STRUCT_0, METRIC_1, FUNCT_2, BINOP_1, BINOP_2, FUNCOP_1, REAL_1,
      VALUED_1, SEQ_1, FINSEQ_1, FINSEQ_2, FINSEQOP, SQUARE_1, RVSUM_1,
      VALUED_2, MONOID_0, PRE_TOPC, PCOMPS_1, TOPMETR, XXREAL_0, ALGSTR_0,
      RLVECT_1, FUNCSDOM, RLTOPSP1;
 constructors REAL_1, SQUARE_1, BINOP_2, COMPLEX1, FINSEQOP, PCOMPS_1,
      MONOID_0, SEQ_1, TOPMETR, RLTOPSP1, FUNCSDOM, VALUED_2;
 registrations XBOOLE_0, FUNCT_1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0,
      BINOP_2, MEMBERED, FINSEQ_2, RVSUM_1, METRIC_1, PCOMPS_1, MONOID_0,
      VALUED_0, VALUED_1, STRUCT_0, TOPMETR, RLTOPSP1, CARD_1, FINSEQ_1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions FINSEQ_1, STRUCT_0, PCOMPS_1, SQUARE_1, FINSEQ_2, RVSUM_1,
      MONOID_0, VALUED_1, VALUED_2, FUNCSDOM, RLVECT_1, CARD_1;
 theorems ABSVALUE, BINOP_1, FINSEQ_1, FINSEQ_2, FINSEQOP, FUNCT_1, FUNCT_2,
      PCOMPS_1, RVSUM_1, SQUARE_1, TARSKI, XREAL_0, COMPLEX1, XREAL_1,
      XXREAL_0, FUNCOP_1, ORDINAL1, VALUED_1, RELAT_1, PRE_TOPC, TOPMETR,
      RSSPACE, RLVECT_1, RLVECT_4, ALGSTR_0, FUNCSDOM, PARTFUN1, RFUNCT_1,
      CARD_1;
 schemes FUNCT_2, BINOP_1;

begin

reserve k,j,n for Nat,
  r for real number;

definition
  let n be Nat;
  func REAL n -> FinSequenceSet of REAL equals
  n-tuples_on REAL;
  coherence;
end;

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

registration
  let n;
  cluster -> n-element for Element of REAL n;
  coherence;
end;

definition
  func absreal -> Function of REAL,REAL means
  :Def2:
  for r holds it.r = abs r;
  existence
  proof
    deffunc F(Real) = abs $1;
    consider f be Function of REAL,REAL such that
A1: for r be Real holds f.r = F(r) from FUNCT_2:sch 4;
    take f;
    let r;
    r is Real by XREAL_0:def 1;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let f, g be Function of REAL,REAL such that
A2: for r holds f.r = abs r and
A3: for r holds g.r = abs r;
    now
      let x be Element of REAL;
      thus f.x = abs x by A2
        .= g.x by A3;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

definition
  let x be real-valued FinSequence;
  redefine func abs x -> FinSequence of REAL equals
  absreal*x;
  coherence
  proof
    thus rng abs x c= REAL;
  end;
  compatibility
  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 g = dom x by RELAT_1:27,VALUED_1:def 11;
    now
      let a be set;
      assume
A2:   a in dom abs x;
      thus (abs x).a = abs (x . a) by VALUED_1:18
        .= absreal.(x . a) by Def2
        .= g.a by A1,A2,FUNCT_1:12;
    end;
    hence thesis by A1,FUNCT_1:2;
  end;
end;

definition
  let n;
  func 0*n -> real-valued FinSequence equals
  n |-> (0 qua Real);
  coherence;
end;

definition
  let n;
  redefine func 0*n -> Element of REAL n;
  coherence;
end;

reserve x,x1,x2,y for Element of REAL n;

definition
  let n,x;
  redefine func -x -> Element of REAL n;
  coherence
  proof
    reconsider 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 thesis;
  end;
end;

definition
  let n,x,y;
  redefine func x + y -> Element of REAL n;
  coherence
  proof
    reconsider 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 thesis;
  end;
  redefine func x - y -> Element of REAL n;
  coherence
  proof
    reconsider 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 thesis;
  end;
end;

definition
  let n, x;
  let r be real number;
  redefine func r*x -> Element of REAL n;
  coherence
  proof
    reconsider 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 thesis;
  end;
end;

definition
  let n,x;
  redefine func abs x -> Element of n-tuples_on REAL;
  coherence by FINSEQ_2:113;
end;

definition
  let n,x;
  redefine func sqr x -> Element of n-tuples_on REAL;
  coherence by FINSEQ_2:113;
end;

reserve f for real-valued FinSequence;

definition
  let f;
  func |. f .| -> Real equals
  sqrt Sum sqr f;
  coherence;
end;

Lm1: f is Element of REAL len f
proof
  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 thesis;
end;

canceled 3;

theorem
  abs 0*n = n |-> (0 qua Real)
proof
  reconsider m=n as Element of NAT by ORDINAL1:def 12;
  thus abs 0*n = m |-> absreal.(0 qua Real) by FINSEQOP:16
    .= n |-> abs 0 by Def2
    .= n |-> 0 by ABSVALUE:2;
end;

theorem Th5:
  for f being complex-valued Function holds abs -f = abs f
  proof
    let f be complex-valued Function;
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
      let x be set;
      assume x in dom abs(-f);
      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;
    end;
    hence thesis by A1,A2,A3,FUNCT_1:2;
  end;

theorem Th6:
  abs(r*f) = abs(r)*(abs f) by RFUNCT_1:25;

theorem Th7:
  |.0*n.| = 0
proof
  thus |.0*n .| = sqrt Sum (n |-> 0^2) by RVSUM_1:56
    .= sqrt (n*0) by RVSUM_1:80
    .= 0 by SQUARE_1:17;
end;

Lm2: sqr abs f = sqr f
proof
  set n = len f;
  reconsider x=f as Element of REAL n by Lm1;
  now
    let k;
    assume k in Seg n;
    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;
  end;
  hence thesis by FINSEQ_2:119;
end;

theorem Th8:
  |. x .| = 0 implies x = 0*n
proof
  assume
A1: |. x .| = 0;
  now
    let j;
    assume
 j in Seg n;
    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 qua Real)).j;
  end;
  hence thesis by FINSEQ_2:119;
end;

theorem Th9:
  |.f.| >= 0
proof
  0 <= Sum sqr f by RVSUM_1:86;
  hence thesis by SQUARE_1:def 2;
end;

registration
  let f;
  cluster |.f.| -> non negative;
  coherence by Th9;
end;

theorem Th10:
  |.-f.| = |.f.|
proof
  thus |.-f.| = sqrt Sum sqr abs -f by Lm2
    .= sqrt Sum sqr abs f by Th5
    .= |.f.| by Lm2;
end;

theorem
  |.r*f.| = abs(r)*|.f.|
proof
  set n = len f;
  reconsider x=f as Element of REAL n 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;
end;

theorem Th12:
  |.x1 + x2.| <= |.x1.| + |.x2.|
proof
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: k in Seg n implies (sqr abs (x1 + x2)).k <= (sqr (abs x1 + abs x2)).k
  proof
    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;
    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 <= r2 by VALUED_1:11;
    hence thesis by VALUED_1:11;
  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: k in Seg n implies 0 <= (mlt(abs x1,abs x2)).k
  proof
    assume k in Seg n;
    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: r = abs(r1)*abs(r2) by RVSUM_1:60;
    0 <= abs(r1) & 0 <= abs(r2) by COMPLEX1:46;
    hence thesis by A11;
  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 thesis by Lm2;
end;

theorem Th13:
  |.x1 - x2.| <= |.x1.| + |.x2.|
proof
  |.x1 - x2.| <= |.x1.| + |.-x2.| by Th12;
  hence thesis by Th10;
end;

theorem
  |.x1.| - |.x2.| <= |.x1 + x2.|
proof
  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 thesis by XREAL_1:20;
end;

theorem
  |.x1.| - |.x2.| <= |.x1 - x2.|
proof
  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 thesis by XREAL_1:20;
end;

theorem Th16:
  |.x1 - x2.| = 0 iff x1 = x2
proof
  reconsider R1=x1,R2=x2 as Element of n-tuples_on REAL;
  thus |.x1 - x2.| = 0 implies x1 = x2
  proof
    assume |.x1 - x2.| = 0;
    then R1 - R2 = 0*n by Th8
      .= n |-> 0;
    hence thesis by RVSUM_1:38;
  end;
  assume x1 = x2;
  then R1 - R2 = 0*n by RVSUM_1:37;
  hence thesis by Th7;
end;

registration
  let n,x1;
  cluster |. x1 - x1 .| -> zero;
  coherence by Th16;
end;

theorem
  x1 <> x2 implies |.x1 - x2.| > 0
proof
  assume x1 <> x2;
  then 0 <> |.x1 - x2.| by Th16;
  hence thesis;
end;

theorem Th18:
  |.x1 - x2.| = |.x2 - x1.|
proof
  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;
end;

theorem Th19:
  |.x1 - x2.| <= |.x1 - x .| + |.x - x2.|
proof
  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 thesis by Th12;
end;

definition
  let n be Nat;
  func Pitag_dist n -> Function of [:REAL n,REAL n:],REAL means
  :Def6:
  for x,y being Element of REAL n holds it.(x,y) = |.x-y.|;
  existence
  proof
    deffunc F(Element of REAL n, Element of REAL n) = |.$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) = F(x,y) from
    BINOP_1:sch 4;
    take f;
    let x,y be Element of REAL n;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let f,g be Function of [:REAL n, REAL n:], REAL;
    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.|;
    reconsider n as Element of NAT by ORDINAL1:def 12;
    reconsider f,g as Function of [:REAL n, REAL n:], REAL;
    now
      let x,y be Element of REAL n;
      thus f.(x,y) = |.x-y.| by A2
        .= g.(x,y) by A3;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

theorem
  for x, y being real-valued FinSequence holds sqr(x-y) = sqr(y-x)
proof
  let x, y be real-valued FinSequence;
  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;
end;

theorem Th21:
  for n being Nat holds Pitag_dist n is_metric_of REAL n
proof
  let n be Nat;
  let x,y,z be Element of REAL n;
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;
  thus (Pitag_dist n).(x,y) = |.x-y.| by Def6
    .= |.y-x .| by Th18
    .= (Pitag_dist n).(y,x) by Def6;
  (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;
end;

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

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

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

registration
  let n be Nat;
  cluster TOP-REAL n -> non empty;
  coherence
  proof
    the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by Def8;
    hence thesis;
  end;
end;

registration
  let n be Nat;
  cluster TOP-REAL n -> TopSpace-like Abelian add-associative right_zeroed
    right_complementable vector-distributive scalar-distributive
    scalar-associative scalar-unital;
  coherence
  proof
    the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by Def8;
    hence TOP-REAL n is TopSpace-like by PRE_TOPC:28;
    the RLSStruct of TOP-REAL n = RealVectSpace Seg n by Def8;
    hence thesis by RSSPACE:15;
  end;
end;

reserve p,p1,p2,p3 for Point of TOP-REAL n,
  x,x1,x2,y,y1,y2 for real number;

theorem Th22:
  the carrier of TOP-REAL n = REAL n
proof
  the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by Def8;
  hence thesis;
end;

theorem Th23:
  p is Function of Seg n, REAL
proof
  the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by Def8;
  then p is Element of Funcs(Seg n,REAL) by FINSEQ_2:93;
  hence thesis;
end;

theorem Th24:
  p is FinSequence of REAL
proof
  p is Function of Seg n, REAL by Th23;
  hence thesis by FINSEQ_2:25;
end;

registration
  let n;
  cluster TOP-REAL n -> constituted-FinSeqs;
  coherence
  proof
    let a be Element of TOP-REAL n;
    thus thesis by Th24;
  end;
end;

registration
  let n;
  cluster -> FinSequence-like for Point of TOP-REAL n;
  coherence;
end;

registration
  let n;
  cluster -> real-valued for Point of TOP-REAL n;
  coherence by Th24;
end;

Lm3: for r1,r2 being real-valued Function st p1 = r1 & p2 =r2 holds p1+p2 = r1
+r2
proof
A1: REAL n = Funcs(Seg n,REAL) by FINSEQ_2:93;
  let r1,r2 be real-valued Function such that
A2: p1 = r1 & p2 =r2;
  reconsider s1 = r1, s2 = r2 as Element of REAL n by A2,Th22;
  the RLSStruct 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;
end;

Lm4: for r being real-valued Function st p = r holds x*p = x(#)r
proof
  reconsider x1 = x as Real by XREAL_0:def 1;
  let r be real-valued Function such that
A1: p = 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;
  the RLSStruct 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;
end;

registration
  let r,s be real number;
  let n;
  let p be Element of TOP-REAL n;
  let f be real-valued FinSequence;
  identify r*p with s*f when r=s, p=f;
  compatibility by Lm4;
end;

registration
  let n;
  let p,q be Element of TOP-REAL n;
  let f,g be real-valued FinSequence;
  identify p+q with f+g when p=f, q=g;
  compatibility by Lm3;
end;

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

registration
  let n;
  let p,q be Element of TOP-REAL n;
  let f,g be real-valued FinSequence;
  identify p-q with f-g when p=f, q=g;
  compatibility;
end;

registration
  let n;
  cluster -> n-element for Point of TOP-REAL n;
  coherence
  proof
    let p be Point of TOP-REAL n;
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;
  end;
end;

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

definition
  let n;
  redefine func 0.REAL n -> Point of TOP-REAL n;
  coherence
  proof
    the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by Def8;
    hence thesis;
  end;
end;

theorem
  for x being Element of REAL n holds sqr abs x = sqr x by Lm2;

theorem
  p1 + p2 + p3 = p1 + (p2 + p3) by RLVECT_1:def 3;

theorem
  0.TOP-REAL n + p = p & p + 0.TOP-REAL n = p by RLVECT_1:4;

theorem
  x*0.TOP-REAL n = 0.TOP-REAL n by RLVECT_1:10;

theorem
  1 * p = p & 0 * p = 0.TOP-REAL n by RLVECT_1:10,def 8;

theorem
  (x*y)*p = x*(y*p) by RLVECT_1:def 7;

theorem
  x*p = 0.TOP-REAL n implies x = 0 or p = 0.TOP-REAL n by RLVECT_1:11;

theorem
  x*(p1 + p2) = x*p1 + x*p2 by RLVECT_1:def 5;

theorem
  (x + y)*p = x*p + y*p by RLVECT_1:def 6;

theorem
  x*p1 = x*p2 implies x = 0 or p1 = p2 by RLVECT_1:36;

canceled;

theorem
  p + -p = 0.TOP-REAL n by RLVECT_1:5;

theorem
  p1 + p2 = 0.TOP-REAL n implies p1 = -p2 by RLVECT_1:6;

theorem
  -(p1 + p2) = -p1 - p2 by RLVECT_1:30;

theorem
  -p = (-1)*p;

theorem
  -x*p = (-x)*p & -x*p = x*(-p) by RLVECT_1:25,79;

theorem
  p1 - p2 = p1 + -p2;

theorem
  p - p = 0.TOP-REAL n by RLVECT_1:5;

theorem
  p1 - p2 = 0.TOP-REAL n implies p1 = p2 by RLVECT_1:21;

theorem
  -(p1 - p2) = p2 - p1 & -(p1 - p2) = -p1 + p2 by RLVECT_1:33;

theorem
  p1 + (p2 - p3) = p1 + p2 - p3 by RLVECT_1:def 3;

theorem
  p1 - (p2 + p3) = p1 - p2 - p3 by RLVECT_1:27;

theorem
  p1 - (p2 - p3) = p1 - p2 + p3 by RLVECT_1:29;

theorem
  p = p + p1 - p1 & p = p - p1 + p1 by RLVECT_4:1;

theorem
  x*(p1 - p2) = x*p1 - x*p2 by RLVECT_1:34;

theorem
  (x-y)*p = x*p - y*p by RLVECT_1:35;

reserve p,p1,p2 for Point of TOP-REAL 2;

theorem
  ex x,y being Real st p=<*x,y*>
proof
  the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by Def8;
  then p is Tuple of 2,REAL by FINSEQ_2:131;
  hence thesis by FINSEQ_2:100;
end;

definition

  let p;
  func p`1 -> Real equals
  p.1;
  coherence;
  func p`2 -> Real equals
  p.2;
  coherence;
end;

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

definition
  let x,y be real number;
  redefine func |[ x,y ]| -> Point of TOP-REAL 2;
  coherence
  proof
A1: y is Real by XREAL_0:def 1;
    the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 & x is Real by Def8,
XREAL_0:def 1;
    hence thesis by A1,FINSEQ_2:101;
  end;
end;

theorem
  |[x,y]|`1 = x & |[x,y]|`2 = y by FINSEQ_1:44;

theorem Th53:
  p = |[p`1, p`2]|
proof
  the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by Def8;
  then p is Tuple of 2,REAL by FINSEQ_2:131;
  then consider x,y be Real such that
A1: p = <* x,y *> by FINSEQ_2:100;
  p`1 = x by A1,FINSEQ_1:44;
  hence thesis by A1,FINSEQ_1:44;
end;

theorem
  0.TOP-REAL 2 = |[0,0]|
proof
  the RLSStruct of TOP-REAL 2 = RealVectSpace Seg 2 & 0.REAL 2 = |[0,0]|
  by Def8,FINSEQ_2:61;
  hence thesis;
end;

theorem Th55:
  p1 + p2 = |[ p1`1 + p2`1, p1`2 + p2`2]|
proof
  the TopStruct 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 thesis by A2,Th53;
end;

theorem
  |[x1, y1]| + |[x2, y2]| = |[ x1 + x2, y1 + y2]|
proof
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 thesis by A1,Th55;
end;

theorem Th57:
  x*p = |[ x*p`1 ,x*p`2 ]|
proof
  (x*p)`1 = x*(p`1) & (x*p)`2 = x*(p`2) by RVSUM_1:44;
  hence thesis by Th53;
end;

theorem
  x*|[x1,y1]| = |[ x*x1,x*y1 ]|
proof
  |[x1,y1]|`1 = x1 & |[x1,y1]|`2 = y1 by FINSEQ_1:44;
  hence thesis by Th57;
end;

theorem Th59:
  -p = |[ -p`1, -p`2]|
proof
  thus -p = (-1)*p .= |[ (-1)*p`1, (-1)*p`2]| by Th57
    .= |[ -p`1, -p`2]|;
end;

theorem
  -|[x1,y1]| = |[ -x1, -y1]|
proof
  |[x1,y1]|`1 = x1 & |[x1,y1]|`2 = y1 by FINSEQ_1:44;
  hence thesis by Th59;
end;

theorem Th61:
  p1 - p2 = |[ p1`1 - p2`1, p1`2 - p2`2]|
proof
  -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]|;
end;

theorem
  |[x1, y1]| - |[x2, y2]| = |[ x1 - x2, y1 - y2]|
proof
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 thesis by A1,Th61;
end;

theorem
  for P being Subset of TOP-REAL n, Q being non empty Subset of Euclid n
  holds P = Q implies (TOP-REAL n) |P = TopSpaceMetr((Euclid n) |Q)
proof
  let P be Subset of (TOP-REAL n), Q be non empty Subset of Euclid n;
  set M = TopSpaceMetr((Euclid n) |Q);
  the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by Def8;
  then M is SubSpace of the TopStruct 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;
  then [#](M) = P by TOPMETR:def 2;
  hence thesis by PRE_TOPC:def 5;
end;

:: to enable the 03.2009. revision A.T.

theorem
  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
  for p being Point of TOP-REAL n for r being real-valued Function st
  p = r holds x*p = x(#)r;

theorem Th66:
  0.REAL n = 0.TOP-REAL n
proof
  the RLSStruct of TOP-REAL n = RealVectSpace Seg n by Def8;
  hence thesis;
end;

theorem Th67:
  the carrier of Euclid n = the carrier of TOP-REAL n
proof
  thus the carrier of Euclid n = the carrier of TopSpaceMetr Euclid n
    .= the carrier of the TopStruct of TOP-REAL n by Def8
    .= the carrier of TOP-REAL n;
end;

theorem
  for p1 being Point of TOP-REAL n for r1 being real-valued Function st
  p1 = r1 holds -p1 = -r1;

theorem
  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
  0.TOP-REAL n = 0*n by Th66;

theorem
  for p being Point of TOP-REAL n holds |.-p.| = |.p.| by Th10;

registration
  let n; let D be set;
  cluster n-tuples_on D -> FinSequence-membered;
  coherence;
end;

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

registration
  let n;
  cluster REAL n -> real-functions-membered;
  coherence
  proof
    let x be set;
    assume x in REAL n;
    then reconsider x as Element of REAL n;
    x is real-valued;
    hence thesis;
  end;
end;

:: from JORDAN2C, 2011.07.28, A.T.

definition
  let n be Nat;
  func 1*n -> FinSequence of REAL equals
  n |-> (1 qua Real);
  coherence;
end;

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

definition
  let n be Nat;
  func 1.REAL n -> Point of TOP-REAL n equals
  1*n;
  coherence by Th22;
end;

theorem
  abs 1*n = n |-> (1 qua Real)
proof
  thus abs 1*n = n |-> absreal.(1 qua Real) by FINSEQOP:16
    .= n |-> abs(1 qua Real) by Def2
    .= n |-> 1 by ABSVALUE:def 1;
end;

theorem Th73:
  |.1*n.| = sqrt n
proof
  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;
end;

theorem
  |. (1.REAL n) .| = sqrt n by Th73;

theorem
  1<=n implies 1<=|. (1.REAL n) .|
proof
  assume
A1: 1<=n;
  |.1.REAL n.|=sqrt n by Th73;
  hence thesis by A1,SQUARE_1:18,26;
end;

theorem
  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;
  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 thesis;
end;

theorem
  REAL 0 = {0.TOP-REAL 0}
proof
  thus REAL 0 = { <*>REAL } by FINSEQ_2:94
    .= {0.TOP-REAL 0};
end;