:: Introduction to Banach and Hilbert spaces - Part I
::  by Jan Popio{\l}ek
::
:: Received July 19, 1991
:: Copyright (c) 1991-2016 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, RLVECT_1, STRUCT_0, SUBSET_1, ALGSTR_0, BINOP_1,
      FUNCT_1, ZFMISC_1, XBOOLE_0, REAL_1, PRE_TOPC, SUPINF_2, PROB_2, RLSUB_1,
      FUNCOP_1, CARD_1, ARYTM_3, RELAT_1, XXREAL_0, ARYTM_1, COMPLEX1,
      SQUARE_1, FUNCT_3, RVSUM_1, NORMSP_1, METRIC_1, NAT_1, BHSP_1, PARTFUN1,
      FUNCT_7;
 notations XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      COMPLEX1, REAL_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1,
      NAT_1, STRUCT_0, ALGSTR_0, DOMAIN_1, PRE_TOPC, RLVECT_1, RLSUB_1,
      SQUARE_1, VFUNCT_1, NORMSP_1, QUIN_1, XXREAL_0;
 constructors BINOP_1, DOMAIN_1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, MEMBERED,
      COMPLEX1, QUIN_1, RLSUB_1, NORMSP_1, RELSET_1, VFUNCT_1;
 registrations SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0,
      SQUARE_1, STRUCT_0, XBOOLE_0, ALGSTR_0, FUNCT_2, VFUNCT_1, QUIN_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions STRUCT_0, ALGSTR_0, RLVECT_1, VALUED_0, FUNCT_2;
 equalities STRUCT_0, SQUARE_1, ALGSTR_0, RLVECT_1;
 expansions VALUED_0;
 theorems TARSKI, SQUARE_1, ABSVALUE, RLVECT_1, RLSUB_1, QUIN_1, FUNCT_2,
      NORMSP_1, COMPLEX1, FUNCOP_1, XREAL_1, XXREAL_0, ALGSTR_0, ORDINAL1,
      VFUNCT_1, PARTFUN1;
 schemes FUNCT_2;

begin

definition
  struct(RLSStruct) UNITSTR (#
  carrier -> set,
  ZeroF -> Element of the carrier,
  addF -> BinOp of the carrier,
  Mult -> Function of [:REAL, the carrier:], the carrier,
  scalar -> Function of [: the carrier, the carrier :], REAL #);
end;

registration
  cluster non empty strict for UNITSTR;
  existence
  proof

set D = the non empty set,Z = the Element of D,a = the BinOp of D,m =the
Function of [:REAL, D:], D,s = the Function of [: D,D:],REAL;
    take UNITSTR (#D,Z,a,m,s#);
    thus the carrier of UNITSTR (#D,Z,a,m,s#) is non empty;
    thus thesis;
  end;
end;

registration
  let D be non empty set, Z be Element of D, a be BinOp of D,m be Function of
  [:REAL, D:], D, s be Function of [: D,D:],REAL;
  cluster UNITSTR (#D,Z,a,m,s#) -> non empty;
  coherence;
end;

reserve X for non empty UNITSTR;
reserve a, b for Real;
reserve x, y for Point of X;

deffunc 09(UNITSTR) = 0.$1;

definition
  let X;
  let x, y;
  func x .|. y -> Real equals
  (the scalar of X).[x,y];
  correctness;
end;

set V0 = the RealLinearSpace;

Lm1: the carrier of (0).V0 = {0.V0} by RLSUB_1:def 3;

reconsider nilfunc
  = [: the carrier of (0).V0, the carrier of (0).V0 :] --> In(0,REAL)
as Function of [: the carrier of (0).V0, the carrier of (0).V0 :] , REAL;

( for x, y being VECTOR of (0).V0 holds nilfunc.[x,y] = 0)& 0.V0 in the
carrier of (0).V0 by Lm1,FUNCOP_1:7,TARSKI:def 1;
then

Lm2: nilfunc.[0.V0,0.V0] = 0;

Lm3: for u, v being VECTOR of (0).V0 holds nilfunc.[u,v] = nilfunc.[v,u]
proof
  let u, v be VECTOR of (0).V0;
  u = 0.V0 & v = 0.V0 by Lm1,TARSKI:def 1;
  hence thesis;
end;

Lm4: for u, v, w being VECTOR of (0).V0 holds nilfunc.[u+v,w] = nilfunc.[u,w]
+ nilfunc.[v,w]
proof
  let u, v, w be VECTOR of (0).V0;
A1: w = 0.V0 by Lm1,TARSKI:def 1;
  u = 0.V0 & v = 0.V0 by Lm1,TARSKI:def 1;
  hence thesis by A1,Lm1,Lm2,TARSKI:def 1;
end;

Lm5: for u, v being VECTOR of (0).V0, a holds nilfunc.[a*u,v] = a * nilfunc.[u
,v]
proof
  let u, v be VECTOR of (0).V0;
  let a;
  u = 0.V0 & v = 0.V0 by Lm1,TARSKI:def 1;
  hence thesis by Lm1,Lm2,TARSKI:def 1;
end;

set X0 = UNITSTR(# the carrier of (0).V0,0.(0).V0,the addF of (0).V0, the Mult
  of (0).V0, nilfunc #);

Lm6: now
  let x, y, z be Point of X0;
  let a;
  09(X0) = 0.V0 by RLSUB_1:11;
  hence x .|. x = In(0,REAL) iff x = 09(X0) by Lm1,FUNCOP_1:7,TARSKI:def 1;
  thus 0 <= x .|. x by FUNCOP_1:7;
  thus x .|. y = y .|. x by Lm3;
  thus (x+y) .|. z = x .|. z + y .|. z
  proof
    reconsider u = x, v = y, w = z as VECTOR of (0).V0;
    (x+y) .|. z = nilfunc.[u+v,w];
    hence thesis by Lm4;
  end;
  thus (a*x) .|. y = a * ( x .|. y )
  proof
    reconsider u = x, v = y as VECTOR of (0).V0;
    (a*x) .|. y = nilfunc.[a*u,v];
    hence thesis by Lm5;
  end;
end;

definition
  let IT be non empty UNITSTR;
  attr IT is RealUnitarySpace-like means
  :Def2:
  for x, y, z being Point of IT, a holds
  ( x .|. x = 0 iff x = 0.IT ) & 0 <= x .|. x & x .|. y = y .|. x &
  (x+y) .|. z = x .|. z + y .|. z & (a*x) .|. y = a * ( x .|. y );
end;

registration
  cluster RealUnitarySpace-like vector-distributive scalar-distributive
  scalar-associative scalar-unital Abelian add-associative
    right_zeroed right_complementable strict for non empty UNITSTR;
  existence
  proof
    take X0;
    thus X0 is RealUnitarySpace-like by Lm6;
    thus X0 is vector-distributive scalar-distributive scalar-associative
    scalar-unital
    proof
      thus for a being Real for v,w being VECTOR of X0 holds a * (v + w
      ) = a * v + a * w
      proof
        let a be Real;
        let v,w be VECTOR of X0;
        reconsider v9= v, w9 = w as VECTOR of (0).V0;
        thus a * (v + w) = a *( v9 + w9) .= a * v9 + a * w9 by RLVECT_1:def 5
          .= a * v + a * w;
      end;
      thus for a,b being Real for v being VECTOR of X0 holds (a + b) *
      v = a * v + b * v
      proof
        let a,b be Real;
        let v be VECTOR of X0;
        reconsider v9= v as VECTOR of (0).V0;
        thus (a + b) * v = (a + b) * v9 .= a * v9 + b * v9 by RLVECT_1:def 6
          .= a * v + b * v;
      end;
      thus for a,b being Real for v being VECTOR of X0 holds (a * b) *
      v = a * (b * v)
      proof
        let a,b be Real;
        let v be VECTOR of X0;
        reconsider v9= v as VECTOR of (0).V0;
        thus (a * b) * v = (a * b) * v9
          .= a * (b * v9) by RLVECT_1:def 7
          .= a * (b * v);
      end;
      let v be VECTOR of X0;
      reconsider v9= v as VECTOR of (0).V0;
      thus 1 * v = 1 * v9 .= v by RLVECT_1:def 8;
    end;
A1: for x,y be VECTOR of X0 for x9,y9 be VECTOR of (0).V0 st x = x9 & y =
    y9 holds x + y= x9 + y9 & for a holds a * x = a * x9;
    thus for v,w being VECTOR of X0 holds v + w = w + v
    proof
      let v,w be VECTOR of X0;
      reconsider v9= v, w9= w as VECTOR of (0).V0;
      thus v + w = w9+ v9 by A1
        .= w + v;
    end;
    thus for u,v,w being VECTOR of X0 holds (u + v) + w = u + (v + w)
    proof
      let u,v,w be VECTOR of X0;
      reconsider u9= u, v9= v, w9= w as VECTOR of (0).V0;
      thus (u + v) + w = (u9 + v9) + w9 .= u9 + (v9 + w9) by RLVECT_1:def 3
        .= u + (v + w);
    end;
    thus for v being VECTOR of X0 holds v + 0.X0 = v
    proof
      let v be VECTOR of X0;
      reconsider v9= v as VECTOR of (0).V0;
      thus v + 0.X0 = v9+ 0.(0).V0 .=v by RLVECT_1:4;
    end;
    thus X0 is right_complementable
    proof
      let v be VECTOR of X0;
      reconsider v9= v as VECTOR of (0).V0;
      consider w9 be VECTOR of (0).V0 such that
A2:   v9 + w9 = 0.(0).V0 by ALGSTR_0:def 11;
      reconsider w = w9 as VECTOR of X0;
      take w;
      thus thesis by A2;
    end;
    thus thesis;
  end;
end;

definition
  mode RealUnitarySpace is RealUnitarySpace-like vector-distributive
  scalar-distributive scalar-associative scalar-unital Abelian
    add-associative right_zeroed right_complementable non empty UNITSTR;
end;

reserve X for RealUnitarySpace;
reserve x, y, z, u, v for Point of X;

definition
  let X, x, y;
  redefine func x .|. y;
  commutativity by Def2;
end;

theorem
  (0.X) .|. (0.X) = 0 by Def2;

theorem
  x .|. (y+z) = x .|. y + x .|. z by Def2;

theorem
  x .|. (a*y) = a * x .|. y by Def2;

theorem
  (a*x) .|. y = x .|. (a*y)
proof
  (a*x) .|. y = a * x .|. y by Def2;
  hence thesis by Def2;
end;

theorem Th5:
  (a*x+b*y) .|. z = a * x .|. z + b * y .|. z
proof
  (a*x+b*y) .|. z = (a*x) .|. z + (b*y) .|. z by Def2
    .= a * x .|. z + (b*y) .|. z by Def2;
  hence thesis by Def2;
end;

theorem
  x .|. (a*y + b*z) = a * x .|. y + b * x .|. z by Th5;

theorem
  (-x) .|. y = x .|. (-y)
proof
  (-x) .|. y = ((-1)*x) .|. y by RLVECT_1:16
    .= (-1) * x .|. y by Def2
    .= x .|. ((-1)*y) by Def2;
  hence thesis by RLVECT_1:16;
end;

theorem Th8:
  (-x) .|. y = - x .|. y
proof
  (-x) .|. y = ((-1)*x) .|. y by RLVECT_1:16
    .= (-1) * x .|. y by Def2;
  hence thesis;
end;

theorem
  x .|. (-y) = - x .|. y by Th8;

theorem Th10:
  (-x) .|. (-y) = x .|. y
proof
  (-x) .|. (-y) = - x .|. (-y) by Th8
    .= - ( - x .|. y ) by Th8;
  hence thesis;
end;

theorem Th11:
  (x - y) .|. z = x .|. z - y .|. z
proof
  (x - y) .|. z = x .|. z + (-y) .|. z by Def2
    .= x .|. z + ( - y .|. z ) by Th8;
  hence thesis;
end;

theorem Th12:
  x .|. (y - z) = x .|. y - x .|. z
proof
  x .|. (y - z) = x .|. y + x .|. (-z) by Def2
    .= x .|. y + ( - x .|. z ) by Th8;
  hence thesis;
end;

theorem
  (x - y) .|. (u - v) = x .|. u - x .|. v - y .|. u + y .|. v
proof
  (x - y) .|. (u - v) = x .|. (u - v) - y .|. (u - v) by Th11
    .= ( x .|. u - x .|. v ) - y .|. (u - v) by Th12
    .= ( x .|. u - x .|. v ) - ( y .|. u - y .|. v ) by Th12;
  hence thesis;
end;

theorem Th14:
  (0.X) .|. x = 0
proof
  09(X) .|. x = (x + (-x)) .|. x by RLVECT_1:5
    .= x .|. x + (-x) .|. x by Def2
    .= x .|. x + ( - x .|. x ) by Th8;
  hence thesis;
end;

theorem
  x .|. 0.X = 0 by Th14;

theorem Th16:
  (x + y) .|. (x + y) = x .|. x + 2 * x .|. y + y .|. y
proof
  (x + y) .|. (x + y) = x .|. (x + y) + y .|. (x + y) by Def2
    .= (x .|. x + x .|. y) + y .|. (x + y) by Def2
    .= (x .|. x + x .|. y) + (x .|. y + y .|. y) by Def2
    .= (x .|. x + (x .|. y + x .|. y)) + y .|. y;
  hence thesis;
end;

theorem
  (x + y) .|. (x - y) = x .|. x - y .|. y
proof
  (x + y) .|. (x - y) = x .|. (x - y) + y .|. (x - y) by Def2
    .= (x .|. x - x .|. y) + y .|. (x - y) by Th12
    .= (x .|. x - x .|. y) + (x .|. y - y .|. y) by Th12;
  hence thesis;
end;

theorem Th18:
  (x - y) .|. (x - y) = x .|. x - 2 * x .|. y + y .|. y
proof
  (x - y) .|. (x - y) = x .|. (x - y) - y .|. (x - y) by Th11
    .= x .|. x - x .|. y - y .|. (x - y) by Th12
    .= x .|. x - x .|. y - ( x .|. y - y .|. y ) by Th12
    .= x .|. x - ( x .|. y + x .|. y ) + y .|. y;
  hence thesis;
end;

theorem Th19:
  |.x .|. y.| <= sqrt (x .|. x) * sqrt (y .|. y)
proof
A1: x <> 09(X) implies |.x .|. y.| <= sqrt (x .|. x) * sqrt (y .|. y)
  proof
A2: for t be Real holds x .|. x * t^2 + (2 * x .|. y) * t + y .|. y >= 0
    proof
      let t be Real;
      reconsider t as Real;
      (t * x + y) .|. (t * x + y) >= 0 by Def2;
      then (t * x) .|. (t * x) + 2 * (t * x) .|. y + y .|. y >= 0 by Th16;
      then t * x .|. (t * x) + 2 * (t * x) .|. y + y .|. y >= 0 by Def2;
      then t * ( t * x .|. x) + 2 * (t * x) .|. y + y .|. y >= 0 by Def2;
      then x .|. x * t^2 + 2 * (x .|. y * t) + y .|. y >= 0 by Def2;
      hence thesis;
    end;
A3: x .|. x >= 0 by Def2;
    assume x <> 09(X);
    then x .|. x <> 0 by Def2;
    then delta(x .|. x,(2 * x .|. y),y.|.y) <= 0 by A3,A2,QUIN_1:10;
    then (2 * x .|. y)^2 - 4 * x .|. x * y .|. y <= 0 by QUIN_1:def 1;
    then 4 * ((x .|. y)^2 - x .|. x * y .|. y) <= 0;
    then (x .|. y)^2 - x .|. x * y .|. y <= 0/4 by XREAL_1:77;
    then (x .|. y)^2 <= x .|. x * y .|. y by XREAL_1:50;
    then (|.x .|. y.|)^2 >= 0 & (|.x .|. y.|)^2 <= x .|. x * y .|. y by
COMPLEX1:75,XREAL_1:63;
    then sqrt (|.x .|. y.|)^2 <= sqrt (x .|. x * y .|. y) by SQUARE_1:26;
    then
A4: |.x .|. y.| <= sqrt (x .|. x * y .|. y) by COMPLEX1:46,SQUARE_1:22;
    y .|. y >= 0 by Def2;
    hence thesis by A3,A4,SQUARE_1:29;
  end;
  x = 09(X) implies |.x .|. y.| <= sqrt (x .|. x) * sqrt (y .|. y)
  proof
    assume x = 09(X);
    then x .|. y = 0 & sqrt (x .|. x) = 0 by Th14,SQUARE_1:17;
    hence thesis by ABSVALUE:2;
  end;
  hence thesis by A1;
end;

definition
  let X, x, y;
  pred x, y are_orthogonal means

  x .|. y = 0;
  symmetry;
end;

theorem
  x, y are_orthogonal implies x, - y are_orthogonal
proof
  assume x, y are_orthogonal;
  then - x .|. y = - 0;
  then x .|. (-y) = 0 by Th8;
  hence thesis;
end;

theorem
  x, y are_orthogonal implies -x, y are_orthogonal
proof
  assume x, y are_orthogonal;
  then - x .|. y = - 0;
  then (-x) .|. y = 0 by Th8;
  hence thesis;
end;

theorem
  x, y are_orthogonal implies -x, -y are_orthogonal
by Th10;

theorem
  x, 0.X are_orthogonal
by Th14;

theorem
  x, y are_orthogonal implies (x + y) .|. (x + y) = x .|. x + y .|. y
proof
  assume x, y are_orthogonal;
  then
A1: x .|. y = 0;
  (x + y) .|. (x + y) = x .|. x + 2 * x .|. y + y .|. y by Th16;
  hence thesis by A1;
end;

theorem
  x, y are_orthogonal implies (x - y) .|. (x - y) = x .|. x + y .|. y
proof
  assume x, y are_orthogonal;
  then
A1: x .|. y = 0;
  (x - y) .|. (x - y) = x .|. x - 2 * x .|. y + y .|. y by Th18
    .= x .|. x + y .|. y - 0 by A1;
  hence thesis;
end;

definition
  let X, x;
  func ||.x.|| -> Real equals
  sqrt (x .|. x);
  correctness;
end;

theorem Th26:
  ||.x.|| = 0 iff x = 0.X
proof
  thus ||.x.|| = 0 implies x = 09(X)
  proof
    assume
A1: ||.x.|| = 0;
    0 <= x .|. x by Def2;
    then x .|. x = 0 by A1,SQUARE_1:24;
    hence thesis by Def2;
  end;
  assume x = 09(X);
  hence thesis by Def2,SQUARE_1:17;
end;

theorem Th27:
  ||.a * x.|| = |.a.| * ||.x.||
proof
A1: 0 <= a^2 & 0 <= x .|. x by Def2,XREAL_1:63;
  ||.a * x.|| = sqrt (a * (x .|. (a * x))) by Def2
    .= sqrt (a * (a * (x .|. x))) by Def2
    .= sqrt (a^2 * (x .|. x))
    .= sqrt (a^2) * sqrt (x .|. x) by A1,SQUARE_1:29
    .= |.a.| * sqrt (x .|. x) by COMPLEX1:72;
  hence thesis;
end;

theorem Th28:
  0 <= ||.x.||
proof
  0 <= x .|. x by Def2;
  hence thesis by SQUARE_1:def 2;
end;

theorem
  |.x .|. y.| <= ||.x.|| * ||.y.|| by Th19;

theorem Th30:
  ||.x + y.|| <= ||.x.|| + ||.y.||
proof
A1: sqrt ||.x + y.||^2 = sqrt ((x + y) .|. (x + y)) by Th28,SQUARE_1:22;
  (x + y) .|. (x + y) >= 0 & ||.x + y.||^2 >= 0 by Def2,XREAL_1:63;
  then ||.x + y.||^2 = (x + y) .|. (x + y) by A1,SQUARE_1:28;
  then
A2: ||.x + y.||^2 = x .|. x + 2 * x .|. y + y .|. y by Th16;
  x .|. x >= 0 by Def2;
  then
A3: ||.x + y.||^2 = (sqrt (x .|. x))^2 + 2 * x .|. y + y .|. y by A2,
SQUARE_1:def 2;
A4: ||.x.|| >= 0 & ||.y.|| >= 0 by Th28;
  |.x .|. y.| <= ||.x.|| * ||.y.|| & x .|. y <= |.x .|. y.| by Th19,
ABSVALUE:4;
  then x .|. y <= ||.x.|| * ||.y.|| by XXREAL_0:2;
  then 2 * x .|. y <= 2 * (||.x.|| * ||.y.||) by XREAL_1:64;
  then ||.x.||^2 + 2 * x .|. y <= ||.x.||^2 + 2 * ||.x.|| * ||.y.|| by
XREAL_1:7;
  then
A5: ||.x.||^2 + 2 * x .|. y + ||.y.||^2 <= ||.x.||^2 + 2 * ||.x.|| * ||.y
  .|| + ||.y.||^2 by XREAL_1:6;
  y .|. y >= 0 by Def2;
  then ||.x + y.||^2 <= (||.x.|| + ||.y.||)^2 by A3,A5,SQUARE_1:def 2;
  hence thesis by A4,SQUARE_1:16;
end;

theorem Th31:
  ||.-x.|| = ||.x.||
proof
A1: |.-1.| = -(-1) by ABSVALUE:def 1;
  ||.-x.|| = ||.(-1) * x.|| by RLVECT_1:16
    .= 1 * ||.x.|| by A1,Th27;
  hence thesis;
end;

theorem Th32:
  ||.x.|| - ||.y.|| <= ||.x - y.||
proof
  (x - y) + y = x - (y - y) by RLVECT_1:29
    .= x - 09(X) by RLVECT_1:15
    .= x by RLVECT_1:13;
  then ||.x.|| <= ||.x - y.|| + ||.y.|| by Th30;
  hence thesis by XREAL_1:20;
end;

theorem
  |.||.x.|| - ||.y.||.| <= ||.x - y.||
proof
  (y - x) + x = y - (x - x) by RLVECT_1:29
    .= y - 09(X) by RLVECT_1:15
    .= y by RLVECT_1:13;
  then ||.y.|| <= ||.y - x.|| + ||.x.|| by Th30;
  then ||.y.|| - ||.x.|| <= ||.y - x.|| by XREAL_1:20;
  then ||.y.|| - ||.x.|| <= ||.-(x - y).|| by RLVECT_1:33;
  then ||.y.|| - ||.x.|| <= ||.x - y.|| by Th31;
  then
A1: -||.x - y.|| <= -(||.y.|| - ||.x.||) by XREAL_1:24;
  ||.x.|| - ||.y.|| <= ||.x - y.|| by Th32;
  hence thesis by A1,ABSVALUE:5;
end;

definition
  let X, x, y;
  func dist(x,y) -> Real equals
  ||.x - y.||;
  correctness;
  commutativity
  proof
    let IT be Real;
    let x,y;
    ||.x - y.|| = ||.-(y-x).|| by RLVECT_1:33
      .= ||.y - x.|| by Th31;
    hence thesis;
  end;
end;

theorem Th34:
  dist(x,x) = 0
proof
  thus dist(x,x) = ||.09(X).|| by RLVECT_1:15
    .= 0 by Th26;
end;

theorem
  dist(x,z) <= dist(x,y) + dist(y,z)
proof
  dist(x,z) = ||.(x-z)+09(X).|| by RLVECT_1:4
    .= ||.(x-z)+(y-y).|| by RLVECT_1:15
    .= ||.x-(z-(y-y)).|| by RLVECT_1:29
    .= ||.x-(y+(z-y)).|| by RLVECT_1:29
    .= ||.(x-y)-(z-y).|| by RLVECT_1:27
    .= ||.(x-y)+(y-z).|| by RLVECT_1:33;
  hence thesis by Th30;
end;

theorem Th36:
  x <> y iff dist(x,y) <> 0
proof
  thus x <> y implies dist(x,y) <> 0
  proof
    assume that
A1: x <> y and
A2: dist(x,y) = 0;
    x - y = 09(X) by A2,Th26;
    hence contradiction by A1,RLVECT_1:21;
  end;
  thus thesis by Th34;
end;

theorem
  dist(x,y) >= 0 by Th28;

theorem
  x <> y iff dist(x,y) > 0
proof
  thus x <> y implies dist(x,y) > 0
  proof
    assume x <> y;
    then dist(x,y) <> 0 by Th36;
    hence thesis by Th28;
  end;
  thus thesis by Th34;
end;

theorem
  dist(x,y) = sqrt ((x-y) .|. (x-y));

theorem
  dist(x + y,u + v) <= dist(x,u) + dist(y,v)
proof
  dist(x + y,u + v) = ||.((-u) + (-v)) + (x + y).|| by RLVECT_1:31
    .= ||.x + ((-u) + (-v)) + y.|| by RLVECT_1:def 3
    .= ||.x - u + (-v) + y.|| by RLVECT_1:def 3
    .= ||.x - u + (y - v).|| by RLVECT_1:def 3;
  hence thesis by Th30;
end;

theorem
  dist(x - y,u - v) <= dist(x,u) + dist(y,v)
proof
  dist(x - y,u - v) = ||.((x - y) - u) + v.|| by RLVECT_1:29
    .= ||.(x - (u + y)) + v.|| by RLVECT_1:27
    .= ||.((x - u) - y) + v.|| by RLVECT_1:27
    .= ||.(x - u) - (y - v).|| by RLVECT_1:29
    .= ||.(x - u) + -(y - v).||;
  then dist(x - y,u - v) <= ||.x - u.|| + ||.-(y - v).|| by Th30;
  hence thesis by Th31;
end;

theorem
  dist(x - z, y - z) = dist(x,y)
proof
  thus dist(x - z,y - z) = ||.((x - z) - y) + z.|| by RLVECT_1:29
    .= ||.(x - (y + z)) + z.|| by RLVECT_1:27
    .= ||.((x - y) - z) + z.|| by RLVECT_1:27
    .= ||.(x - y) - (z - z).|| by RLVECT_1:29
    .= ||.(x - y) - 09(X).|| by RLVECT_1:15
    .= dist(x,y) by RLVECT_1:13;
end;

theorem
  dist(x - z,y - z) <= dist(z,x) + dist(z,y)
proof
  dist(x - z,y - z) = ||.(x - z) + (z - y).|| by RLVECT_1:33
    .= ||.-(z - x) + (z - y).|| by RLVECT_1:33;
  then dist(x - z,y - z) <= ||.-(z - x).|| + ||.z - y.|| by Th30;
  hence thesis by Th31;
end;

reserve seq, seq1, seq2, seq3 for sequence of X;
reserve  n for Nat;

definition
  let X be non empty addLoopStr;
  let seq be sequence of X;
  let x be Point of X;

  func seq + x -> sequence of X means
  :Def6:
  for n holds it.n = seq.n + x;
  existence
  proof
    deffunc F(Nat) = seq.$1 + x;
    consider seq be sequence of X such that
A1:   for n being Element of NAT holds seq.n = F(n) from FUNCT_2:sch 4;
    take seq;
    let n;
     n in NAT by ORDINAL1:def 12;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let seq1, seq2 be sequence of X;
    assume that
A2: for n holds seq1.n = seq.n + x and
A3: for n holds seq2.n = seq.n + x;
    let n be Element of NAT;
    seq1.n = seq.n + x by A2;
    hence thesis by A3;
  end;
end;

theorem Th44:
  for X being non empty addLoopStr, seq being sequence of X holds
  (-seq).n = - seq.n
  proof
    let X be non empty addLoopStr, seq be sequence of X;
A1: dom -seq = NAT by FUNCT_2:def 1;
A2: dom seq = NAT by FUNCT_2:def 1;
A3:  n in NAT by ORDINAL1:def 12;
    hence (-seq).n = (-seq)/.n by PARTFUN1:def 6,A1
    .= -seq/.n by A1,VFUNCT_1:def 5,A3
    .= - seq.n by A3,PARTFUN1:def 6,A2;
  end;

definition
  let X, seq1, seq2;
  redefine func seq1 + seq2;
  commutativity
proof let seq1, seq2;
    let n be Element of NAT;
    thus (seq1 + seq2).n = seq2.n + seq1.n by NORMSP_1:def 2
      .= (seq2 + seq1).n by NORMSP_1:def 2;
end;
end;

theorem
  seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3
proof
  let n be Element of NAT;
  thus (seq1 + (seq2 + seq3)).n = seq1.n + (seq2 + seq3).n by NORMSP_1:def 2
    .= seq1.n + (seq2.n + seq3.n) by NORMSP_1:def 2
    .= (seq1.n + seq2.n) + seq3.n by RLVECT_1:def 3
    .= (seq1 + seq2).n + seq3.n by NORMSP_1:def 2
    .= ((seq1 + seq2) + seq3).n by NORMSP_1:def 2;
end;

theorem
  seq1 is constant & seq2 is constant implies seq1 + seq2 is constant
proof
  assume that
A1: seq1 is constant and
A2: seq2 is constant;
    set seq = seq1 + seq2;
  consider x such that
A3: for n being Nat holds seq1.n = x by A1;
  consider y such that
A4: for n being Nat holds seq2.n = y by A2;
  take z = x + y;
  let n be Nat;
  thus seq.n = seq1.n + seq2.n by NORMSP_1:def 2
    .= x + seq2.n by A3
    .= z by A4;
end;

theorem
  seq1 is constant & seq2 is constant implies seq1 - seq2 is constant
proof
  assume that
A1: seq1 is constant and
A2: seq2 is constant;
    set seq = seq1 - seq2;
  consider x such that
A3: for n being Nat holds seq1.n = x by A1;
  consider y such that
A4: for n being Nat holds seq2.n = y by A2;
  take z = x - y;
  let n be Nat;
  thus seq.n = seq1.n - seq2.n by NORMSP_1:def 3
    .= x - seq2.n by A3
    .= z by A4;
end;

theorem
  seq1 is constant implies a * seq1 is constant
proof
  assume
A1: seq1 is constant;
    set seq = a * seq1;
  consider x such that
A2: for n being Nat holds seq1.n = x by A1;
  take z = a * x;
  let n be Nat;
  thus seq.n = a * seq1.n by NORMSP_1:def 5
    .= z by A2;
end;

theorem
  seq1 - seq2 = seq1 + -seq2
proof
  let n be Element of NAT;
  thus (seq1 - seq2).n = seq1.n - seq2.n by NORMSP_1:def 3
    .= seq1.n + (-seq2).n by Th44
    .= (seq1 + -seq2).n by NORMSP_1:def 2;
end;

theorem
  seq = seq + 0.X
proof
  let n be Element of NAT;
  thus (seq + 09(X)).n = seq.n + 09(X) by Def6
    .= seq.n by RLVECT_1:4;
end;

theorem
  a * (seq1 + seq2) = a * seq1 + a * seq2
proof
  let n be Element of NAT;
  thus (a * (seq1 + seq2)).n = a * (seq1 + seq2).n by NORMSP_1:def 5
    .= a * (seq1.n + seq2.n) by NORMSP_1:def 2
    .= a * seq1.n + a * seq2.n by RLVECT_1:def 5
    .= (a * seq1).n + a * seq2.n by NORMSP_1:def 5
    .= (a * seq1).n + (a * seq2).n by NORMSP_1:def 5
    .= (a * seq1 + a * seq2).n by NORMSP_1:def 2;
end;

theorem
  (a + b) * seq = a * seq + b * seq
proof
  let n be Element of NAT;
  thus ((a + b) * seq).n = (a + b) * seq.n by NORMSP_1:def 5
    .= a * seq.n + b * seq.n by RLVECT_1:def 6
    .= (a * seq).n + b * seq.n by NORMSP_1:def 5
    .= (a * seq).n + (b * seq).n by NORMSP_1:def 5
    .= (a * seq + b * seq).n by NORMSP_1:def 2;
end;

theorem
  (a * b) * seq = a * (b * seq)
proof
  let n be Element of NAT;
  thus ((a * b) * seq).n = (a * b) * seq.n by NORMSP_1:def 5
    .= a * (b * seq.n) by RLVECT_1:def 7
    .= a * (b * seq).n by NORMSP_1:def 5
    .= (a * (b * seq)).n by NORMSP_1:def 5;
end;

theorem
  (1 qua Real) * seq = seq
proof
  let n be Element of NAT;
  thus (1 * seq).n = 1 * seq.n by NORMSP_1:def 5
    .= seq.n by RLVECT_1:def 8;
end;

theorem
  (-1) * seq = - seq
proof
  let n be Element of NAT;
  thus ((-1) * seq).n = (-1) * seq.n by NORMSP_1:def 5
    .= - seq.n by RLVECT_1:16
    .= (-seq).n by Th44;
end;

theorem
  seq - x = seq + -x
proof
  let n be Element of NAT;
  thus (seq - x).n = seq.n - x by NORMSP_1:def 4
    .= (seq + -x).n by Def6;
end;

theorem
  seq1 - seq2 = - (seq2 - seq1)
proof
  let n be Element of NAT;
  thus (seq1 - seq2).n = seq1.n - seq2.n by NORMSP_1:def 3
    .= - (seq2.n - seq1.n) by RLVECT_1:33
    .= - (seq2 - seq1).n by NORMSP_1:def 3
    .= (- (seq2 - seq1)).n by Th44;
end;

theorem
  seq = seq - 0.X
proof
  let n be Element of NAT;
  thus (seq - 09(X)).n = seq.n - 09(X) by NORMSP_1:def 4
    .= seq.n by RLVECT_1:13;
end;

theorem
  seq = - ( - seq )
proof
  let n be Element of NAT;
  thus (- ( - seq )).n = - (- seq).n by Th44
    .= - ( - seq.n) by Th44
    .= seq.n by RLVECT_1:17;
end;

theorem
  seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
proof
  let n be Element of NAT;
  thus (seq1 - (seq2 + seq3)).n = seq1.n - (seq2 + seq3).n by NORMSP_1:def 3
    .= seq1.n - (seq2.n + seq3.n) by NORMSP_1:def 2
    .= (seq1.n - seq2.n) - seq3.n by RLVECT_1:27
    .= (seq1 - seq2).n - seq3.n by NORMSP_1:def 3
    .= ((seq1 - seq2) - seq3).n by NORMSP_1:def 3;
end;

theorem
  (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3)
proof
  let n be Element of NAT;
  thus ((seq1 + seq2) - seq3).n = (seq1 + seq2).n - seq3.n by NORMSP_1:def 3
    .= (seq1.n + seq2.n) - seq3.n by NORMSP_1:def 2
    .= seq1.n + (seq2.n - seq3.n) by RLVECT_1:def 3
    .= seq1.n + (seq2 - seq3).n by NORMSP_1:def 3
    .= (seq1 + (seq2 - seq3)).n by NORMSP_1:def 2;
end;

theorem
  seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
proof
  let n be Element of NAT;
  thus (seq1 - (seq2 - seq3)).n = seq1.n - (seq2 - seq3).n by NORMSP_1:def 3
    .= seq1.n - (seq2.n - seq3.n) by NORMSP_1:def 3
    .= (seq1.n - seq2.n) + seq3.n by RLVECT_1:29
    .= (seq1 - seq2).n + seq3.n by NORMSP_1:def 3
    .= ((seq1 - seq2) + seq3).n by NORMSP_1:def 2;
end;

theorem
  a * (seq1 - seq2) = a * seq1 - a * seq2
proof
  let n be Element of NAT;
  thus (a * (seq1 - seq2)).n = a * (seq1 - seq2).n by NORMSP_1:def 5
    .= a * (seq1.n - seq2.n) by NORMSP_1:def 3
    .= a * seq1.n - a * seq2.n by RLVECT_1:34
    .= (a * seq1).n - a * seq2.n by NORMSP_1:def 5
    .= (a * seq1).n - (a * seq2).n by NORMSP_1:def 5
    .= (a * seq1 - a * seq2).n by NORMSP_1:def 3;
end;