:: Complex Linear Space of Complex Sequences
::  by Noboru Endou
::
:: Received January 26, 2004
:: Copyright (c) 2004-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, XBOOLE_0, COMSEQ_1, FUNCT_2, TARSKI, RSSPACE, CFUNCT_1,
      BINOP_1, SUBSET_1, FUNCT_1, ARYTM_3, ZFMISC_1, VALUED_1, COMPLEX1,
      FUNCOP_1, RLVECT_1, CLVECT_1, RELAT_1, SUPINF_2, ARYTM_1, STRUCT_0,
      ALGSTR_0, RLSUB_1, REALSET1, SERIES_1, SEQ_1, CARD_1, XXREAL_0, REAL_1,
      SQUARE_1, BHSP_1, PRE_TOPC, PROB_2, XCMPLX_0, RVSUM_1, NORMSP_1,
      METRIC_1, NAT_1, CARD_3, SEQ_2, ORDINAL2, CSSPACE;
 notations TARSKI, XBOOLE_0, SUBSET_1, PRE_TOPC, RELAT_1, DOMAIN_1, FUNCT_1,
      FUNCT_2, FUNCOP_1, VALUED_1, SEQ_1, BINOP_1, REALSET1, XCMPLX_0,
      XXREAL_0, REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, ZFMISC_1, NUMBERS,
      SQUARE_1, COMPLEX1, COMSEQ_1, CFUNCT_1, COMSEQ_2, SERIES_1, COMSEQ_3,
      RLVECT_1, VFUNCT_1, NORMSP_1, BHSP_1, CLVECT_1;
 constructors BINOP_1, FUNCOP_1, REAL_1, SQUARE_1, SEQ_1, COMSEQ_2, COMSEQ_3,
      REALSET1, BHSP_1, CLVECT_1, RELSET_1, VFUNCT_1;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2,
      NUMBERS, XCMPLX_0, XXREAL_0, MEMBERED, REALSET1, STRUCT_0, CLVECT_1,
      ALGSTR_0, VALUED_1, VALUED_0, VFUNCT_1, SERIES_1;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
 definitions TARSKI, RLVECT_1, CLVECT_1, STRUCT_0, REALSET1, SQUARE_1, BINOP_1,
      ALGSTR_0, VALUED_0;
 theorems XBOOLE_0, RELAT_1, SQUARE_1, TARSKI, ABSVALUE, ZFMISC_1, SEQ_1,
      SERIES_1, COMSEQ_3, FUNCT_1, FUNCT_2, RLVECT_1, BINOP_1, XCMPLX_0,
      COMSEQ_1, CLVECT_1, COMPLEX1, COMSEQ_2, NORMSP_1, FUNCOP_1, XREAL_1,
      XXREAL_0, BHSP_1, ALGSTR_0, VALUED_1, VALUED_0, ORDINAL1;
 schemes NAT_1, BINOP_1, XBOOLE_0, BINOP_2;

begin

definition
  func the_set_of_ComplexSequences -> non empty set means
  :Def1:
  for x being set holds x in it iff x is Complex_Sequence;
  existence
  proof
    defpred P[set] means $1 is Complex_Sequence;
    consider IT being set such that
A1: for x being set holds x in IT iff x in Funcs(NAT,COMPLEX) & P[x]
    from XBOOLE_0:sch 1;
    IT is non empty
    proof
      set zeroseq = the Complex_Sequence;
      zeroseq in Funcs(NAT,COMPLEX) by FUNCT_2:8;
      hence thesis by A1;
    end;
    then reconsider IT as non empty set;
    take IT;
    for x being set holds x is Complex_Sequence implies x in IT
    proof
      let x be set;
      assume
A2:   x is Complex_Sequence;
      then x in Funcs(NAT,COMPLEX) by FUNCT_2:8;
      hence thesis by A1,A2;
    end;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let X1,X2 be non empty set;
    assume that
A3: for x being set holds x in X1 iff x is Complex_Sequence and
A4: for x being set holds x in X2 iff x is Complex_Sequence;
A5: X2 c= X1
    proof
      let x be set;
      assume x in X2;
      then x is Complex_Sequence by A4;
      hence thesis by A3;
    end;
    X1 c= X2
    proof
      let x be set;
      assume x in X1;
      then x is Complex_Sequence by A3;
      hence thesis by A4;
    end;
    hence thesis by A5,XBOOLE_0:def 10;
  end;
end;

definition
  let z be set such that
A1: z in the_set_of_ComplexSequences;
  func seq_id(z) -> Complex_Sequence equals
  :Def2:
  z;
  coherence by A1,Def1;
end;

definition
  let z be set such that
A1: z is Complex;
  func C_id(z) -> Complex equals
  :Def3:
  z;
  coherence by A1;
end;

definition
  func l_add -> BinOp of the_set_of_ComplexSequences means
  :Def4:
  for a,b
being Element of the_set_of_ComplexSequences holds it.(a,b) = seq_id(a)+seq_id(
  b);
  existence
proof
  defpred P[Element of the_set_of_ComplexSequences, Element of
the_set_of_ComplexSequences, Element of the_set_of_ComplexSequences] means $3=
  seq_id($1)+seq_id($2);
A1: for x,y being Element of the_set_of_ComplexSequences ex z being Element
  of the_set_of_ComplexSequences st P[x,y,z]
  proof
    let x,y be Element of the_set_of_ComplexSequences;
    seq_id(x)+seq_id(y) is Element of the_set_of_ComplexSequences by Def1;
    hence thesis;
  end;
  ex ADD be BinOp of the_set_of_ComplexSequences st for a,b being Element
  of the_set_of_ComplexSequences holds P[a,b,ADD.(a,b)] from BINOP_1:sch 3(A1);
  then consider ADD be BinOp of the_set_of_ComplexSequences such that
A2: for a,b being Element of the_set_of_ComplexSequences holds ADD.(a,b)
  = seq_id(a)+seq_id(b);
  thus thesis by A2;
end;
  uniqueness
  proof
    deffunc O(Element of the_set_of_ComplexSequences, Element of
    the_set_of_ComplexSequences)=seq_id($1)+seq_id($2);
    for o1,o2 being BinOp of the_set_of_ComplexSequences st (for a,b being
    Element of the_set_of_ComplexSequences holds o1.(a,b) = O(a,b)) & (for a,b
being Element of the_set_of_ComplexSequences holds o2.(a,b) = O(a,b)) holds o1
    = o2 from BINOP_2:sch 2;
    hence thesis;
  end;
end;

definition
  func l_mult -> Function of [:COMPLEX,the_set_of_ComplexSequences:],
  the_set_of_ComplexSequences means
  :Def5:
  for z,x be set st z is Complex & x in the_set_of_ComplexSequences holds
  it.(z,x) = C_id(z)(#)seq_id(x);
  existence
proof
  deffunc F(set,set) = C_id($1) (#) seq_id($2);
A1: for r,x be set st r in COMPLEX & x in the_set_of_ComplexSequences holds
  F(r,x) in the_set_of_ComplexSequences by Def1;
  consider f be Function of [:COMPLEX, the_set_of_ComplexSequences:],
  the_set_of_ComplexSequences such that
A2: for r,x be set st r in COMPLEX & x in
  the_set_of_ComplexSequences holds f.(r,x) = F(r,x) from BINOP_1:sch 2(A1);
  take f;
  let r,x be set;
  assume r is Complex;
  then r in COMPLEX by XCMPLX_0:def 2;
  hence thesis by A2;
end;
  uniqueness
  proof
    let mult1,mult2 be Function of [:COMPLEX,the_set_of_ComplexSequences:],
    the_set_of_ComplexSequences such that
A3: for z,x be set st z is Complex & x in the_set_of_ComplexSequences
    holds mult1.(z,x) = C_id(z)(#)seq_id(x) and
A4: for z,x be set st z is Complex & x in the_set_of_ComplexSequences
    holds mult2.(z,x) = C_id(z)(#)seq_id(x);
    for z being Element of COMPLEX for x being Element of
    the_set_of_ComplexSequences holds mult1.(z,x) = mult2.(z,x)
    proof
      let z being Element of COMPLEX;
      let x being Element of the_set_of_ComplexSequences;
      thus mult1.(z,x) = C_id(z)(#)seq_id(x) by A3
        .= mult2.(z,x) by A4;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

definition
  func CZeroseq -> Element of the_set_of_ComplexSequences means
  :Def6:
  for n be Element of NAT holds (seq_id it).n=0c;
  existence
  proof
    reconsider zeroseq = NAT --> 0c as Complex_Sequence;
A1: for n be Element of NAT holds zeroseq.n=0c by FUNCOP_1:7;
A2: zeroseq in the_set_of_ComplexSequences by Def1;
    then seq_id(zeroseq) = zeroseq by Def2;
    hence thesis by A1,A2;
  end;
  uniqueness
  proof
    let x,y be Element of the_set_of_ComplexSequences such that
A3: for n be Element of NAT holds (seq_id(x)).n=0c and
A4: for n be Element of NAT holds (seq_id(y)).n=0c;
A5: for s be Element of NAT holds (seq_id(x)).s = (seq_id(y)).s
    proof
      let s be Element of NAT;
      (seq_id y).s = 0c by A4;
      hence thesis by A3;
    end;
    x=seq_id(x) by Def2
      .=seq_id(y) by A5,FUNCT_2:63;
    hence thesis by Def2;
  end;
end;

theorem Th1:
  for x being Complex_Sequence holds seq_id x = x
proof
  let x be Complex_Sequence;
  x in the_set_of_ComplexSequences by Def1;
  hence thesis by Def2;
end;

theorem
  for v,w being VECTOR of CLSStruct(#the_set_of_ComplexSequences,
    CZeroseq,l_add,l_mult#) holds v + w = seq_id(v)+seq_id(w) by Def4;

theorem Th3:
  for z being Complex, v being VECTOR of CLSStruct(#
the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds z * v = z(#)seq_id(v
  )
proof
  let z be Complex;
  let v be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq, l_add,
    l_mult #);
  thus z*v = l_mult.(z,v) .= C_id(z)(#)seq_id(v) by Def5
    .= z(#)seq_id(v) by Def3;
end;

registration
  cluster CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) ->
    Abelian;
  coherence
  proof
    let v,w being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,
      l_add,l_mult #);
    v + w = seq_id(v)+seq_id(w) by Def4;
    hence thesis by Def4;
  end;
end;

theorem Th4:
  for u,v,w being VECTOR of CLSStruct(# the_set_of_ComplexSequences
    ,CZeroseq,l_add,l_mult #) holds (u + v) + w = u + (v + w)
proof
  let u,v,w be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,
    l_add,l_mult #);
  (u+v) + w = seq_id(u+v)+seq_id(w) by Def4
    .= seq_id(seq_id(u)+seq_id(v)) + seq_id(w) by Def4
    .= (seq_id(u)+seq_id(v)) + seq_id(w) by Th1
    .= seq_id(u)+(seq_id(v)+seq_id(w)) by COMSEQ_1:7
    .= seq_id(u)+seq_id(seq_id(v)+seq_id(w)) by Th1
    .= seq_id(u) + seq_id(v+w) by Def4;
  hence thesis by Def4;
end;

theorem Th5:
  for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,
CZeroseq,l_add,l_mult #) holds v + 0.CLSStruct(# the_set_of_ComplexSequences,
    CZeroseq,l_add,l_mult #) = v
proof
  set V=CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #);
  let v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add
    ,l_mult #);
A1: for s being Element of NAT holds (seq_id(v)+seq_id(CZeroseq)).s=(seq_id(
  v)).s
  proof
    let s be Element of NAT;
    (seq_id(v)+seq_id(CZeroseq)).s = (seq_id(v)).s+(seq_id(CZeroseq)).s by
VALUED_1:1
      .= (seq_id(v)).s + 0c by Def6;
    hence thesis;
  end;
  v + 0.V = seq_id(v)+seq_id(CZeroseq) by Def4;
  hence v + 0.V=seq_id(v) by A1,FUNCT_2:63
    .=v by Def2;
end;

theorem Th6:
  for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,
    CZeroseq,l_add,l_mult #) ex w being VECTOR of CLSStruct(#
the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) st v + w = 0.CLSStruct(#
    the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #)
proof
  set V = CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #);
  let v be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,
    l_mult #);
  reconsider w=-seq_id(v) as VECTOR of V by Def1;
  for s being Element of NAT holds (seq_id(v)+(-seq_id(v)) ).s=(seq_id(
  CZeroseq)).s
  proof
    let s be Element of NAT;
    (seq_id(v)+(-seq_id(v))).s = (seq_id(v)).s+(-seq_id(v)).s by VALUED_1:1
      .= (seq_id(v)).s + (-((seq_id(v)).s)) by VALUED_1:8
      .= (seq_id(CZeroseq)).s by Def6;
    hence thesis;
  end;
  then
A1: seq_id(v)+(-seq_id(v)) = seq_id(CZeroseq) by FUNCT_2:63
    .=CZeroseq by Def2;
  v+w = seq_id(v)+seq_id(w) by Def4
    .= seq_id(v)+(-seq_id(v)) by Th1;
  hence thesis by A1;
end;

theorem Th7:
  for z being Complex, v,w being VECTOR of CLSStruct(#
the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds z * (v + w) = z * v
  + z * w
proof
  let z be Complex;
  let v,w being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,
    l_add,l_mult #);
A1: z in COMPLEX by XCMPLX_0:def 2;
A2: z * (v + w) = z(#)seq_id(v + w) by Th3
    .= z(#)seq_id(seq_id(v) + seq_id(w)) by Def4
    .= z(#)(seq_id(v) + seq_id(w)) by Th1
    .= z(#)seq_id(v) + z(#)seq_id(w) by A1,COMSEQ_1:16;
  z*v + z*w = seq_id(z*v)+seq_id(z*w) by Def4
    .=seq_id(z(#)seq_id(v)) + seq_id(z*w) by Th3
    .=seq_id(z(#)seq_id(v)) + seq_id(z(#)seq_id(w)) by Th3
    .=z(#)seq_id(v) + seq_id(z(#)seq_id(w)) by Th1
    .=z(#)seq_id(v) + z(#)seq_id(w) by Th1;
  hence thesis by A2;
end;

theorem Th8:
  for z1,z2 being Complex, v being VECTOR of CLSStruct(#
the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds (z1 + z2) * v = z1 *
  v + z2 * v
proof
  let z1,z2 be Complex;
  let v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add
    ,l_mult #);
  for s being Element of NAT holds ((z1+z2)(#)seq_id(v)).s=(z1(#)seq_id(v)
  +z2(#)seq_id(v)).s
  proof
    let s be Element of NAT;
    ((z1+z2)(#)seq_id(v)).s = (z1+z2)*(seq_id(v)).s by VALUED_1:6
      .= z1*((seq_id(v)).s)+z2*((seq_id(v)).s)
      .= (z1(#)seq_id(v)).s+z2*(seq_id(v)).s by VALUED_1:6
      .= (z1(#)seq_id(v)).s+(z2(#)seq_id(v)).s by VALUED_1:6;
    hence thesis by VALUED_1:1;
  end;
  then
A1: (z1+z2)(#)seq_id(v) =z1(#)seq_id(v)+z2(#)seq_id(v) by FUNCT_2:63;
  z1*v + z2*v = seq_id(z1*v)+seq_id(z2*v) by Def4
    .=seq_id(z1(#)seq_id(v)) + seq_id(z2*v) by Th3
    .=seq_id(z1(#)seq_id(v)) + seq_id(z2(#)seq_id(v)) by Th3
    .=z1(#)seq_id(v) + seq_id(z2(#)seq_id(v)) by Th1
    .=z1(#)seq_id(v) + z2(#)seq_id(v) by Th1;
  hence thesis by A1,Th3;
end;

theorem Th9:
  for z1,z2 be Complex, v being VECTOR of CLSStruct(#
the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds (z1 * z2) * v = z1 *
  (z2 * v)
proof
  let z1,z2 be Complex;
A1: z1 in COMPLEX & z2 in COMPLEX by XCMPLX_0:def 2;
  let v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add
    ,l_mult #);
  (z1 * z2) * v =(z1*z2)(#)seq_id(v) by Th3
    .=z1(#)(z2(#)seq_id(v)) by A1,COMSEQ_1:17
    .=z1(#)seq_id(z2(#)seq_id(v)) by Th1
    .=z1(#)seq_id(z2*v) by Th3;
  hence thesis by Th3;
end;

theorem Th10:
  for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,
    CZeroseq,l_add,l_mult #) holds 1r * v = v
proof
  let v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add
    ,l_mult #);
  1r * v =1r(#)seq_id(v) by Th3
    .=seq_id(v) by COMSEQ_1:21;
  hence thesis by Def2;
end;

definition
  func Linear_Space_of_ComplexSequences -> strict non empty CLSStruct equals
  CLSStruct (# the_set_of_ComplexSequences, CZeroseq, l_add, l_mult #);
  coherence;
end;

registration
  cluster Linear_Space_of_ComplexSequences -> Abelian add-associative
    right_zeroed right_complementable vector-distributive scalar-distributive
    scalar-associative scalar-unital;
  coherence
  proof
    set L = Linear_Space_of_ComplexSequences;
    thus L is Abelian;
    thus L is add-associative
    proof
      let x be Element of L;
      thus thesis by Th4;
    end;
    thus L is right_zeroed
    proof
      let x be Element of L;
      thus thesis by Th5;
    end;
    thus L is right_complementable
    proof
      let x be Element of L;
      consider y being Element of L such that
A1:   x + y = 0.L by Th6;
      take y;
      thus thesis by A1;
    end;
    thus (for z being Complex, v,w being VECTOR of L holds z * (v + w) = z * v
+ z * w) & (for z1,z2 being Complex, v being VECTOR of L holds (z1 + z2) * v =
z1 * v + z2 * v) & (for z1,z2 being Complex, v being VECTOR of L holds (z1 * z2
) * v = z1 * (z2 * v)) & for v being VECTOR of L holds 1r * v = v by Th7,Th8
,Th9,Th10;
  end;
end;

definition
  let X be ComplexLinearSpace;
  let X1 be Subset of X such that
B1: X1 is linearly-closed;
  func Add_(X1,X) -> BinOp of X1 equals
  :Def8:
  (the addF of X) || X1;
  correctness
  proof
A1: dom (the addF of X) = [:the carrier of X,the carrier of X:] by
FUNCT_2:def 1;
A2: for z be set st z in [:X1,X1:] holds ((the addF of X) || X1).z in X1
    proof
      let z be set such that
A3:   z in [:X1,X1:];
      consider r,x be set such that
A4:   r in X1 and
A5:   x in X1 and
A6:   z=[r,x] by A3,ZFMISC_1:def 2;
      reconsider y=x,r1=r as VECTOR of X by A4,A5;
      [r,x] in dom ((the addF of X) || X1) by A1,A3,A6,RELAT_1:62,ZFMISC_1:96;
      then ((the addF of X) || X1).z = r1+y by A6,FUNCT_1:47;
      hence thesis by B1,A4,A5,CLVECT_1:def 7;
    end;
    dom ((the addF of X) || X1) =[:X1,X1:] by A1,RELAT_1:62,ZFMISC_1:96;
    hence thesis by A2,FUNCT_2:3;
  end;
end;

definition
  let X be ComplexLinearSpace;
  let X1 be Subset of X such that
B1: X1 is linearly-closed;
  func Mult_(X1,X) -> Function of [:COMPLEX,X1:], X1 equals
  :Def9:
  (the Mult
  of X) | [:COMPLEX,X1:];
  correctness
  proof
A1: dom (the Mult of X) = [:COMPLEX,the carrier of X:] by FUNCT_2:def 1;
A2: [:COMPLEX,X1:] c= [:COMPLEX,the carrier of X:] by ZFMISC_1:95;
A3: for z be set st z in [:COMPLEX,X1:] holds ((the Mult of X) | [:COMPLEX
    ,X1:]).z in X1
    proof
      let z be set such that
A4:   z in [:COMPLEX,X1:];
      consider r,x be set such that
A5:   r in COMPLEX and
A6:   x in X1 and
A7:   z=[r,x] by A4,ZFMISC_1:def 2;
      reconsider r as Complex by A5;
      reconsider y=x as VECTOR of X by A6;
      [r,x] in dom ((the Mult of X) | [:COMPLEX,X1:]) by A2,A1,A4,A7,RELAT_1:62
;
      then ((the Mult of X) | [:COMPLEX,X1:]).z = r*y by A7,FUNCT_1:47;
      hence thesis by B1,A6,CLVECT_1:def 7;
    end;
    dom ((the Mult of X) | [:COMPLEX,X1:]) =[:COMPLEX,X1:] by A2,A1,RELAT_1:62;
    hence thesis by A3,FUNCT_2:3;
  end;
end;

definition
  let X be ComplexLinearSpace, X1 be Subset of X such that
A1: X1 is linearly-closed and
A2: X1 is non empty;
  func Zero_(X1,X) -> Element of X1 equals
  :Def10:
  0.X;
  correctness
  proof
    set v = the Element of X1;
    v in X1 by A2;
    then reconsider v as Element of X;
    v-v=0.X by RLVECT_1:15;
    hence thesis by A1,A2,CLVECT_1:22;
  end;
end;

theorem Th11:
  for V be ComplexLinearSpace, V1 be Subset of V st V1 is
linearly-closed & V1 is non empty holds CLSStruct (# V1,Zero_(V1,V), Add_(V1,V)
    ,Mult_(V1,V) #) is Subspace of V
proof
  let V be ComplexLinearSpace;
  let V1 be Subset of V such that
A1: V1 is linearly-closed and
A2: V1 is non empty;
A3: Add_(V1,V)= (the addF of V) || V1 by A1,Def8;
A4: Mult_(V1,V) = (the Mult of V) | [:COMPLEX,V1:] by A1,Def9;
  Zero_(V1,V) = 0.V by A1,A2,Def10;
  hence thesis by A2,A3,A4,CLVECT_1:43;
end;

definition
  func the_set_of_l2ComplexSequences -> Subset of
  Linear_Space_of_ComplexSequences means
  :Def11:
  it is non empty & for x being
  set holds x in it iff x in the_set_of_ComplexSequences & |.seq_id(x).|(#)|.
  seq_id(x).| is summable;
  existence
  proof
    defpred P[set] means |.seq_id($1).|(#)|.seq_id($1).| is summable;
    consider IT being set such that
A1: for x being set holds x in IT iff x in the_set_of_ComplexSequences
    & P[x] from XBOOLE_0:sch 1;
    for x be set st x in IT holds x in the_set_of_ComplexSequences by A1;
    then
A2: IT is Subset of the_set_of_ComplexSequences by TARSKI:def 3;
    |.seq_id(CZeroseq).|(#)|.seq_id(CZeroseq).| is absolutely_summable
    proof
      reconsider rseq=|.seq_id(CZeroseq).|(#)|.seq_id(CZeroseq).| as
      Real_Sequence;
      now
        let n be Element of NAT;
        thus rseq.n =(|.seq_id(CZeroseq).|).n * (|.seq_id(CZeroseq).|).n by
SEQ_1:8
          .=(|.seq_id(CZeroseq).|).n * |.(seq_id(CZeroseq)).n.| by VALUED_1:18
          .=(|.seq_id(CZeroseq).|).n * 0 by Def6,COMPLEX1:44
          .=0;
      end;
      hence thesis by COMSEQ_3:3;
    end;
    then IT is non empty by A1;
    hence thesis by A1,A2;
  end;
  uniqueness
  proof
    let X1,X2 be Subset of Linear_Space_of_ComplexSequences;
    assume that
    X1 is non empty and
A3: for x being set holds x in X1 iff x in
    the_set_of_ComplexSequences & |.seq_id(x).|(#)|.seq_id(x).| is summable and
    X2 is non empty and
A4: for x being set holds x in X2 iff x in
    the_set_of_ComplexSequences & |.seq_id(x).|(#)|.seq_id(x).| is summable;
A5: X2 c= X1
    proof
      let x be set;
      assume
A6:   x in X2;
      then |.seq_id(x).|(#)|.seq_id(x).| is summable by A4;
      hence thesis by A3,A6;
    end;
    X1 c= X2
    proof
      let x be set;
      assume
A7:   x in X1;
      then |.seq_id(x).|(#)|.seq_id(x).| is summable by A3;
      hence thesis by A4,A7;
    end;
    hence thesis by A5,XBOOLE_0:def 10;
  end;
end;

theorem Th12:
  the_set_of_l2ComplexSequences is linearly-closed &
  the_set_of_l2ComplexSequences is non empty
proof
  set W = the_set_of_l2ComplexSequences;
A1: for v,u be VECTOR of Linear_Space_of_ComplexSequences st v in
the_set_of_l2ComplexSequences & u in the_set_of_l2ComplexSequences holds v + u
  in the_set_of_l2ComplexSequences
  proof
    let v,u be VECTOR of Linear_Space_of_ComplexSequences such that
A2: v in W and
A3: u in W;
    |.seq_id(v+u).|(#)|.seq_id(v+u).| is summable
    proof
      set r = |.seq_id(v+u).|(#)|.seq_id(v+u).|;
      set q = |.seq_id(u).|(#)|.seq_id(u).|;
      set p = |.seq_id(v).|(#)|.seq_id(v).|;
A4:   for n be Element of NAT holds 0<=r.n
      proof
        let n be Element of NAT;
        r.n=(|.seq_id(v+u).|).n * (|.seq_id(v+u).|).n by SEQ_1:8;
        hence thesis by XREAL_1:63;
      end;
A5:   for n be Element of NAT holds r.n <=(2(#)p+2(#)q).n
      proof
        set t = |.seq_id(u).|;
        set s = |.seq_id(v).|;
        let n be Element of NAT;
        reconsider sn=s.n, tn=t.n as Real;
A6:     r.n = ((|.seq_id(v+u).|).n)^2 by SEQ_1:8;
        (2(#)p+2(#)q).n=(2(#)p).n +(2(#)q).n by SEQ_1:7
          .= 2*p.n + (2(#)q).n by SEQ_1:9
          .= 2*p.n + 2*q.n by SEQ_1:9
          .= 2*(s.n*s.n) + 2*q.n by SEQ_1:8
          .= 2*sn^2 + 2*tn^2 by SEQ_1:8;
        then
A7:     (2(#)p+2(#)q).n - (sn^2 + 2*sn*tn + tn^2) = (sn-tn)^2;
A8:     seq_id(v+u)=seq_id(seq_id(v)+seq_id(u)) by Def4
          .=seq_id(v)+seq_id(u) by Th1;
        (|.seq_id(v+u).|).n = |.(seq_id(v+u)).n .| by VALUED_1:18
          .= |.(seq_id(v)).n + (seq_id(u)).n.| by A8,VALUED_1:1;
        then (|.seq_id(v+u).|).n <= |.(seq_id(v)).n.| + |.(seq_id(u)).n.| by
COMPLEX1:56;
        then (|.seq_id(v+u).|).n <= s.n + |.((seq_id(u)).n).| by VALUED_1:18;
        then
A9:     (|.seq_id(v+u).|).n <= s.n + t.n by VALUED_1:18;
        0 <= (sn-tn)^2 by XREAL_1:63;
        then
A10:    0 + (sn^2 + 2*sn*tn + tn^2) <= (2(#)p+2(#)q).n by A7,XREAL_1:19;
        0 <= |.(seq_id(v+u)).n.| by COMPLEX1:46;
        then 0 <= (|.seq_id(v+u).|).n by VALUED_1:18;
        then ((|.seq_id(v+u).|).n)^2 <= (s.n + t.n)^2 by A9,SQUARE_1:15;
        hence thesis by A6,A10,XXREAL_0:2;
      end;
      |.seq_id(u).|(#)|.seq_id(u).| is summable by A3,Def11;
      then
A11:  2(#)q is summable by SERIES_1:10;
      |.seq_id(v).|(#)|.seq_id(v).| is summable by A2,Def11;
      then 2(#)p is summable by SERIES_1:10;
      then 2(#)p+2(#)q is summable by A11,SERIES_1:7;
      hence thesis by A4,A5,SERIES_1:20;
    end;
    hence thesis by Def11;
  end;
  for z be Complex for v be VECTOR of Linear_Space_of_ComplexSequences st
  v in W holds z * v in W
  proof
    let z be Complex;
    let v be VECTOR of Linear_Space_of_ComplexSequences;
    assume v in W;
    then
A12: |.seq_id(v).|(#)|.seq_id(v).| is summable by Def11;
A13: z in COMPLEX by XCMPLX_0:def 2;
    seq_id(z*v)=seq_id(z(#)seq_id(v)) by Th3
      .=z(#)seq_id(v) by Th1;
    then |.seq_id(z*v).| = |.z.|(#)|.seq_id(v).| by A13,COMSEQ_1:50;
    then |.seq_id(z*v).|(#)|.seq_id(z*v).| =|.z.|(#)(|.z.|(#)|.seq_id(v).|(#)
    |.seq_id(v).|) by SEQ_1:18
      .=|.z.|(#)(|.z.|(#)(|.seq_id(v).|(#)|.seq_id(v).|)) by SEQ_1:18
      .=(|.z.|*|.z.|)(#)(|.seq_id(v).|(#)|.seq_id(v).|) by SEQ_1:23;
    then |.seq_id(z*v).|(#)|.seq_id(z*v).| is summable by A12,SERIES_1:10;
    hence thesis by Def11;
  end;
  hence thesis by A1,Def11,CLVECT_1:def 7;
end;

theorem
  CLSStruct(# the_set_of_l2ComplexSequences, Zero_(
    the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Add_(
    the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Mult_(
the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences) #) is Subspace
  of Linear_Space_of_ComplexSequences by Th11,Th12;

theorem Th14:
  CLSStruct (# the_set_of_l2ComplexSequences, Zero_(
    the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Add_(
    the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Mult_(
    the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences) #) is
  ComplexLinearSpace by Th11,Th12;

theorem
  the carrier of Linear_Space_of_ComplexSequences =
  the_set_of_ComplexSequences & (for x be set holds x is Element of
  Linear_Space_of_ComplexSequences iff x is Complex_Sequence ) & (for x be set
holds x is VECTOR of Linear_Space_of_ComplexSequences iff x is Complex_Sequence
) & (for u be VECTOR of Linear_Space_of_ComplexSequences holds u =seq_id(u) ) &
  (for u,v be VECTOR of Linear_Space_of_ComplexSequences holds u+v =seq_id(u)+
  seq_id(v) ) & for z be Complex for u be VECTOR of
Linear_Space_of_ComplexSequences holds z*u =z(#)seq_id(u) by Def1,Def2,Def4,Th3
;

begin  :: Unitary space with complex coefficient

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

registration
  cluster non empty strict for CUNITSTR;
  existence
  proof

set D = the non empty set,Z = the Element of D,a = the BinOp of D,m =the
Function of [:COMPLEX, D:], D,s = the Function of [: D,D:],COMPLEX;
    take CUNITSTR (#D,Z,a,m,s#);
    thus the carrier of CUNITSTR (#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
  [:COMPLEX, D:], D, s be Function of [: D,D:],COMPLEX;
  cluster CUNITSTR (#D,Z,a,m,s#) -> non empty;
  coherence;
end;

reserve X for non empty CUNITSTR;
reserve a, b for Complex;
reserve x, y for Point of X;

deffunc 09(CUNITSTR) = 0.$1;

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

set V0 = the ComplexLinearSpace;

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

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

Lm2: for x, y being VECTOR of (0).V0 holds nilfunc.[x,y] = 0c by FUNCOP_1:7;

0.V0 in the carrier of (0).V0 by Lm1,TARSKI:def 1;
then

Lm3: nilfunc.[0.V0,0.V0] = 0c by Lm2;

Lm4: for u being VECTOR of (0).V0 holds 0 <= Re(nilfunc.[u,u]) & Im(nilfunc.[u
,u]) = 0 by COMPLEX1:4,FUNCOP_1:7;

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

Lm6: 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: v = 0.V0 by Lm1,TARSKI:def 1;
A2: w = 0.V0 by Lm1,TARSKI:def 1;
  u = 0.V0 by Lm1,TARSKI:def 1;
  hence thesis by A1,A2,Lm1,Lm3,TARSKI:def 1;
end;

Lm7: 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;
A1: v = 0.V0 by Lm1,TARSKI:def 1;
  u = 0.V0 by Lm1,TARSKI:def 1;
  hence thesis by A1,Lm1,Lm3,TARSKI:def 1;
end;

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

Lm8: now
  let x, y, z be Point of X0;
  let a;
  09(X0) = 0.V0 by CLVECT_1:30;
  hence x .|. x = 0c iff x = 09(X0) by Lm1,Lm2,TARSKI:def 1;
  thus 0 <= Re(x .|. x) & 0 = Im(x .|. x) by Lm4;
  thus x .|. y = (y .|. x)*' by Lm5;
  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 Lm6;
  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 Lm7;
  end;
end;

definition
  let IT be non empty CUNITSTR;
  attr IT is ComplexUnitarySpace-like means
  :Def13:
  for x,y,w being Point of
IT, a holds ( x .|. x = 0 iff x = 0.IT ) & 0 <= Re(x .|. x) & 0 = Im(x .|. x) &
x .|. y = (y .|. x)*' & (x+y) .|. w = x .|. w + y .|. w & (a*x) .|. y = a * ( x
  .|. y );
end;

registration
  cluster ComplexUnitarySpace-like vector-distributive scalar-distributive
  scalar-associative scalar-unital Abelian
add-associative right_zeroed right_complementable strict for
non empty CUNITSTR;
  existence
  proof
    take X0;
    thus X0 is ComplexUnitarySpace-like by Def13,Lm8;
    thus X0 is vector-distributive scalar-distributive scalar-associative
    scalar-unital
    proof
      thus for a for v,w being VECTOR of X0 holds a * (v + w) = a * v + a * w
      proof
        let a;
        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 CLVECT_1:def 2
          .= a * v + a * w;
      end;
      thus for a,b for v being VECTOR of X0 holds (a+ b) * v = a* v + b * v
      proof
        let a,b;
        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 CLVECT_1:def 3
          .= a * v + b * v;
      end;
      thus for a,b for v being VECTOR of X0 holds (a * b) * v = a * (b * v)
      proof
        let a,b;
        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 CLVECT_1:def 4
          .= a * (b * v);
      end;
      let v be VECTOR of X0;
      reconsider v9= v as VECTOR of (0).V0;
      thus 1r * v = 1r * v9 .= v by CLVECT_1:def 5;
    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 ComplexUnitarySpace is ComplexUnitarySpace-like vector-distributive
  scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable non empty CUNITSTR;
end;

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

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

theorem Th17:
  x.|.(y+z) = x.|.y + x.|.z
proof
  thus x.|.(y+z) = ((y+z).|.x)*' by Def13
    .= (y.|.x + z.|.x)*' by Def13
    .= (y.|.x)*' + (z.|.x)*' by COMPLEX1:32
    .= x.|.y + (z.|.x)*' by Def13
    .= x.|.y + x.|.z by Def13;
end;

theorem Th18:
  x.|.(a*y) = (a*') * x.|.y
proof
  thus x.|.(a*y) = ((a*y).|.x)*' by Def13
    .= (a*(y.|.x))*' by Def13
    .= (a*') * (y.|.x)*' by COMPLEX1:35
    .= (a*') * (x.|.y) by Def13;
end;

theorem Th19:
  (a*x).|.y = x.|.((a*')*y)
proof
  (a*x) .|. y = a * x .|. y by Def13
    .= (a*')*' * (y.|.x)*' by Def13
    .= ((a*')*(y.|.x))*' by COMPLEX1:35
    .= (((a*')*y).|.x)*' by Def13;
  hence thesis by Def13;
end;

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

theorem Th21:
  x.|.(a*y + b*z) = (a*') * x.|.y + (b*') * x.|.z
proof
  x.|.(a*y + b*z) = ((a*y + b*z).|.x)*' by Def13
    .= ( a * y.|.x + b * z.|.x )*' by Th20
    .= ( a * y.|.x )*' + ( b * z.|.x )*' by COMPLEX1:32
    .= (a*') * (y.|.x)*' + ( b * z.|.x )*' by COMPLEX1:35
    .= (a*') * (y.|.x)*' + (b*') * (z.|.x)*' by COMPLEX1:35
    .= (a*') * x.|.y + (b*') * (z.|.x)*' by Def13;
  hence thesis by Def13;
end;

theorem Th22:
  (-x) .|. y = x .|. (-y)
proof
  (-x) .|. y = ((-1r)*x) .|. y by CLVECT_1:3
    .= x.|.( (-(1r))*' * y) by Th19
    .= x.|.( (-1r) * y) by COMPLEX1:30,33;
  hence thesis by CLVECT_1:3;
end;

theorem Th23:
  (-x).|.y = - x.|.y
proof
  (-x) .|. y = ((-1r)*x) .|. y by CLVECT_1:3
    .= (-1) * x .|. y by Def13,COMPLEX1:def 4;
  hence thesis;
end;

theorem Th24:
  x.|.(-y) = - x.|.y
proof
  x.|.(-y) = (-x).|.y by Th22;
  hence thesis by Th23;
end;

theorem Th25:
  (-x).|.(-y) = x.|.y
proof
  (-x).|.(-y) = - x.|.(-y) by Th23
    .= - ( - x .|. y ) by Th24;
  hence thesis;
end;

theorem Th26:
  (x-y).|.z = x.|.z - y.|.z
proof
  (x - y) .|. z = x .|. z + (-y) .|. z by Def13
    .= x .|. z + ( - y .|. z ) by Th23;
  hence thesis;
end;

theorem Th27:
  x.|.(y-z) = x.|.y - x.|.z
proof
  x .|. (y - z) = x .|. y + x .|. (-z) by Th17
    .= x .|. y + ( - x .|. z ) by Th24;
  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 Th26
    .= ( x .|. u - x .|. v ) - y .|. (u - v) by Th27
    .= ( x .|. u - x .|. v ) - ( y .|. u - y .|. v ) by Th27;
  hence thesis;
end;

theorem Th29:
  (0.X).|.x = 0
proof
  09(X) .|. x = (x + (-x)) .|. x by RLVECT_1:5
    .= x .|. x + (-x) .|. x by Def13
    .= x .|. x + ( - x .|. x ) by Th23;
  hence thesis;
end;

theorem Th30:
  x.|.0.X = 0
proof
  x.|.0.X = ((0.X).|.x)*' by Def13
    .= 0c by Th29,COMPLEX1:28;
  hence thesis;
end;

theorem Th31:
  (x+y).|.(x+y) = x.|.x + x.|.y + y.|.x + y.|.y
proof
  (x+y).|.(x+y) = x.|.(x+y) + y.|.(x+y) by Def13
    .= (x.|.x + x.|.y) + y.|.(x+y) by Th17
    .= (x.|.x + x.|.y) + (y.|.x + y.|.y) by Th17;
  hence thesis;
end;

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

theorem Th33:
  (x-y).|.(x-y) = x.|.x - x.|.y - y.|.x + y.|.y
proof
  (x - y) .|. (x - y) = x .|. (x - y) - y .|. (x - y) by Th26
    .= x .|. x - x .|. y - y .|. (x - y) by Th27
    .= x.|.x - x.|.y - ( y.|.x - y.|.y ) by Th27;
  hence thesis;
end;

Lm9: for p,q being Complex, x,y being Point of X holds (p*x + q*y).|.(p*x + q
*y) = p*p*' *(x.|.x) + p*q*' *(x.|.y) + p*' *q*(y.|.x) + q*q*' *(y.|.y)
proof
  let p,q be Complex;
  let x,y being Point of X;
  (p*x+q*y).|.(p*x+q*y) = p * (x.|.(p*x + q*y)) + q * (y.|.(p*x + q*y)) by Th20
    .= p * (p*' *(x.|.x) + q*' *(x.|.y)) + q * (y.|.(p*x + q*y)) by Th21
    .= p*p*' *(x.|.x) + p*q*' *(x.|.y) + (q * (p*' *(y.|.x) + q*' *(y.|.y)))
  by Th21
    .= p*p*' *(x.|.x) + p*q*' *(x.|.y) + (q*p*' *(y.|.x) + q*q*' *(y.|.y));
  hence thesis;
end;

theorem Th34:
  |.(x.|.x).| = Re(x.|.x)
proof
A1: Im (x.|.x) = 0 by Def13;
  Re (x.|.x) >= 0 by Def13;
  then |.Re(x.|.x)+Im(x.|.x)*<i>.| = Re (x.|.x) by A1,ABSVALUE:def 1;
  hence thesis by COMPLEX1:13;
end;

theorem Th35: ::Schwarz's inequality
  |.(x.|.y).| <= sqrt|.(x.|.x).| * sqrt|.(y.|.y).|
proof
A1: y <> 09(X) implies |.(x.|.y).| <= sqrt|.(x.|.x).| * sqrt|.(y.|.y).|
  proof
    assume y <> 09(X);
    then y.|.y <> 0c by Def13;
    then
A2: |.(y.|.y).| <> 0 by COMPLEX1:45;
A3: (Re(x.|.y))^2 >= 0 by XREAL_1:63;
    set c2 = -(x.|.y);
    reconsider c1 = |.(y.|.y).|+0*<i> as Element of COMPLEX by XCMPLX_0:def 2;
A4: Re( c1*(c1*(x.|.x) + c2*(y.|.x)) ) = Re c1 * Re (c1*(x.|.x) + c2*(y
    .|.x)) - Im c1 * Im (c1*(x.|.x) + c2*(y.|.x)) by COMPLEX1:9
      .= Re c1 * Re (c1*(x.|.x) + c2*(y.|.x)) - 0 * Im (c1*(x.|.x) + c2*(y
    .|.x)) by COMPLEX1:12
      .= Re c1 * Re (c1*(x.|.x) + c2*(y.|.x));
A5: Re (c2*(y.|.x)) = Re (-(x.|.y)*(y.|.x))
      .= - Re(x.|.y * y.|.x) by COMPLEX1:17
      .= - Re((x.|.y) * (x.|.y)*') by Def13;
A6: Im((x.|.y) * (x.|.y)*') = 0 by COMPLEX1:40;
A7: Im (y.|.y) = 0 by Def13;
A8: Re (y.|.y) >= 0 by Def13;
    then |.Re(y.|.y)+Im(y.|.y)*<i>.| = Re (y.|.y) by A7,ABSVALUE:def 1;
    then
A9: |.(y.|.y).| = Re (y.|.y) by COMPLEX1:13;
    then
A10: (y.|.y) = c1 by A7,COMPLEX1:13;
    ((c1*x+c2*y).|.(c1*x+c2*y)) = c1*c1*' *(x.|.x) + c1*c2*' *(x.|.y) +c1
    *' *c2*(y.|.x) + c2*c2*' *(y.|.y) by Lm9
      .= c1*(c1*' *(x.|.x)) + c1*(c2*' *(x.|.y)) +c1*' *(c2*(y.|.x)) + c1*(
    c2*c2*') by A7,A9,COMPLEX1:13
      .= c1*(c1*' *(x.|.x) + c2*' *(x.|.y)) +c1*(c2*(y.|.x)) + c1*(c2*c2*')
    by A10,Def13
      .= c1*(c1*' *(x.|.x) + c2*' *(x.|.y) + c2*(y.|.x) + c2*c2*')
      .= c1*(c1*(x.|.x) + (x.|.y)*c2*' + c2*(y.|.x) + c2*c2*') by A10,Def13
      .= c1*(c1*(x.|.x) + c2*(y.|.x));
    then Re( c1*(c1*(x.|.x) + c2*(y.|.x)) ) >= 0 by Def13;
    then
    Re c1 >= 0 & Re (c1*(x.|.x) + c2*(y.|.x)) >= 0 or Re c1 <= 0 & Re (c1
    *(x.|.x) + c2*(y.|.x)) <= 0 by A4,XREAL_1:132;
    then Re (c1*(x.|.x)) + Re (c2*(y.|.x)) >= 0 by A8,A7,A9,A2,COMPLEX1:8,13;
    then Re (c1*(x.|.x)) - Re((x.|.y) * (x.|.y)*') >= 0 by A5;
    then
A11: Re (c1*(x.|.x)) >= Re((x.|.y) * (x.|.y)*') + 0 by XREAL_1:19;
A12: Im(x.|.x) = 0 by Def13;
A13: (Im(x.|.y))^2 >= 0 by XREAL_1:63;
    Im c1 = 0 by A7,A9,COMPLEX1:13;
    then Im(c1*(x.|.x)) = Re c1 * 0 + Re (x.|.x)*0 by A12,COMPLEX1:9;
    then
A14: |.c1*(x.|.x).| = abs(Re (c1*(x.|.x))) by COMPLEX1:50;
    Re((x.|.y) * (x.|.y)*') = (Re(x.|.y))^2 + (Im(x.|.y))^2 by COMPLEX1:40;
    then
A15: Re((x.|.y) * (x.|.y)*') >= 0 + 0 by A3,A13,XREAL_1:7;
    then abs(Re((x.|.y) * (x.|.y)*')) = Re((x.|.y) * (x.|.y)*') by
ABSVALUE:def 1;
    then abs(Re (c1*(x.|.x))) >= abs(Re((x.|.y) * (x.|.y)*')) by A11,A15,
ABSVALUE:def 1;
    then |.c1*(x.|.x).| >= |.(x.|.y)*(x.|.y)*' .| by A6,A14,COMPLEX1:50;
    then |.(x.|.x).|*|.(y.|.y).| >= |.(x.|.y)*(x.|.y)*'.| by A10,COMPLEX1:65;
    then |.(x.|.x).|*|.(y.|.y).| >= |.(x.|.y).|*|.(x.|.y)*'.| by COMPLEX1:65;
    then
A16: |.(x.|.x).|*|.(y.|.y).| >= |.(x.|.y).|*|.(x.|.y).| by COMPLEX1:53;
    |.(x.|.y).|^2 >= 0 by XREAL_1:63;
    then
A17: sqrt(|.(x.|.x).|*|.(y.|.y).|) >= sqrt(|.(x.|.y).|^2) by A16,SQUARE_1:26;
A18: |.(y.|.y).| >= 0 by COMPLEX1:46;
    |.(x.|.x).| >= 0 by COMPLEX1:46;
    then sqrt|.(x.|.x).| * sqrt|.(y.|.y).| >= sqrt(|.(x.|.y).|^2) by A17,A18,
SQUARE_1:29;
    hence thesis by COMPLEX1:46,SQUARE_1:22;
  end;
  y = 09(X) implies |.(x.|.y).| <= sqrt|.(x.|.x).| * sqrt|.(y.|.y).|
  proof
    assume
A19: y = 09(X);
    then y.|.y = 0c by Def13;
    hence thesis by A19,Th30,COMPLEX1:44,SQUARE_1:17;
  end;
  hence thesis by A1;
end;

definition
  let X;
  let x, y;
  pred x, y are_orthogonal means
  :Def14:
  x .|. y = 0;
  symmetry by Def13,COMPLEX1:28;
end;

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

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

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

theorem
  x, 0.X are_orthogonal
proof
  (0.X).|.x = 0 by Th29;
  hence thesis by Def14;
end;

theorem
  x,y are_orthogonal implies (x+y).|.(x+y) = x.|.x + y.|.y
proof
  assume
A1: x, y are_orthogonal;
  then
A2: y .|. x = 0c by Def14;
  x .|. y = 0c by A1,Def14;
  then (x + y) .|. (x + y) = x.|.x + 0c + y.|.y by A2,Th31;
  hence thesis;
end;

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

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

theorem Th42:
  ||.x.|| = 0 iff x = 0.X
proof
  thus ||.x.|| = 0 implies x = 09(X)
  proof
    0 <= Re (x.|.x) by Def13;
    then
A1: 0 <= |.(x.|.x).| by Th34;
    assume ||.x.|| = 0;
    then |.(x.|.x).| = 0 by A1,SQUARE_1:24;
    then x.|.x = 0c by COMPLEX1:45;
    hence thesis by Def13;
  end;
  assume x = 09(X);
  hence thesis by Def13,COMPLEX1:44,SQUARE_1:17;
end;

theorem Th43:
  ||.a * x.|| = |.a.| * ||.x.||
proof
A1: 0 <= |.a*a.| by COMPLEX1:46;
  0 <= Re (x.|.x) by Def13;
  then
A2: 0 <= |.(x.|.x).| by Th34;
  ||.a*x.|| = sqrt |.(a*(x.|.(a*x))).| by Def13
    .= sqrt |.(a*(a*' *(x.|.x))).| by Th18
    .= sqrt |.((a*a*')*(x.|.x)).|
    .= sqrt (|.(a*a*').|*|.(x.|.x).|) by COMPLEX1:65
    .= sqrt (|.a*a.| * |.(x.|.x).|) by COMPLEX1:69
    .= sqrt |.a*a.| * sqrt |.(x.|.x).| by A1,A2,SQUARE_1:29
    .= sqrt (|.a.|^2) * sqrt |.(x.|.x).| by COMPLEX1:65
    .= |.a.| * sqrt |.(x.|.x).| by COMPLEX1:46,SQUARE_1:22;
  hence thesis;
end;

theorem Th44:
  0 <= ||.x.||
proof
  0 <= Re(x.|.x) by Def13;
  then 0 <= |.(x.|.x).| by Th34;
  hence thesis by SQUARE_1:def 2;
end;

theorem
  |.(x.|.y).| <= ||.x.|| * ||.y.|| by Th35;

theorem Th46:
  ||.x + y.|| <= ||.x.|| + ||.y.||
proof
A1: ||.x + y.||^2 >= 0 by XREAL_1:63;
  Re ((x+y).|.(x+y)) >= 0 by Def13;
  then
A2: |.((x + y).|.(x + y)).| >= 0 by Th34;
  sqrt ||.x + y.||^2 = sqrt |.((x + y).|.(x + y)).| by Th44,SQUARE_1:22;
  then
A3: ||.x + y.||^2 = |.((x + y).|.(x + y)).| by A2,A1,SQUARE_1:28;
  |.(y.|.y).| >= 0 by COMPLEX1:46;
  then
A4: |.(y.|.y).| = ||.y.||^2 by SQUARE_1:def 2;
A5: -Im(x.|.y) = Im((x.|.y)*') by COMPLEX1:27
    .= Im(y.|.x) by Def13;
  Im(x.|.x + x.|.y + y.|.x + y.|.y) = Im(x.|.x + x.|.y + y.|.x) + Im(y.|.y
  ) by COMPLEX1:8
    .= Im(x.|.x + x.|.y) + Im(y.|.x) + Im(y.|.y) by COMPLEX1:8
    .= Im(x.|.x) + Im(x.|.y) + Im(y.|.x) + Im(y.|.y) by COMPLEX1:8
    .= 0 + Im(x.|.y) + Im(y.|.x) + Im(y.|.y) by Def13
    .= Im(x.|.y) + Im(y.|.x) + 0 by Def13;
  then
A6: (x.|.x + x.|.y + y.|.x + y.|.y) = Re(x.|.x + x.|.y + y.|.x + y.|.y)+0*
  <i> by A5,COMPLEX1:13;
A7: Re(x.|.y) = Re((x.|.y)*') by COMPLEX1:27
    .= Re(y.|.x) by Def13;
A8: Re(x.|.y) <= |.(x.|.y).| by COMPLEX1:54;
  |.(x.|.y).| <= ||.x.||*||.y.|| by Th35;
  then Re(x.|.y) <= ||.x.||*||.y.|| by A8,XXREAL_0:2;
  then
A9: 2*Re(x.|.y) <= 2*(||.x.||*||.y.||) by XREAL_1:64;
  Re(x.|.x + x.|.y + y.|.x + y.|.y) = Re((x + y).|.(x + y)) by Th31;
  then
A10: Re(x.|.x + x.|.y + y.|.x + y.|.y) >= 0 by Def13;
  Re(x.|.x + x.|.y + y.|.x + y.|.y) = Re(x.|.x + x.|.y + y.|.x) + Re(y.|.y
  ) by COMPLEX1:8
    .= Re(x.|.x + x.|.y) + Re(y.|.x) + Re(y.|.y) by COMPLEX1:8
    .= Re(x.|.x) + Re(x.|.y) + Re(y.|.x) + Re(y.|.y) by COMPLEX1:8
    .= |.(x.|.x).| + Re(x.|.y) + Re(y.|.x) + Re(y.|.y) by Th34
    .= |.(x.|.x).| + Re(x.|.y) + Re(y.|.x) + |.(y.|.y).| by Th34;
  then |.(x.|.x + x.|.y + y.|.x + y.|.y).| = |.(x.|.x).| + 2*Re(x.|.y) + |.(y
  .|.y).| by A7,A10,A6,ABSVALUE:def 1;
  then
A11: ||.x + y.||^2 = 2*Re(x.|.y) + (|.(x.|.x).| + |.(y.|.y).|) by A3,Th31;
A12: ||.y.|| >= 0 by Th44;
  |.(x.|.x).| >= 0 by COMPLEX1:46;
  then (sqrt |.(x.|.x).|)^2 = |.(x.|.x).| by SQUARE_1:def 2;
  then
  ||.x + y.||^2 <= 2*(||.x.||*||.y.||) + (||.x.||^2 + |.(y.|.y).|) by A11,A9,
XREAL_1:6;
  then
A13: ||.x + y.||^2 <= (||.x.|| + ||.y.||)^2 by A4;
  ||.x.|| >= 0 by Th44;
  then ||.x.|| + ||.y.|| >= 0 + 0 by A12,XREAL_1:7;
  hence thesis by A13,SQUARE_1:16;
end;

theorem Th47:
  ||.-x.|| = ||.x.||
proof
  ||.-x.|| = ||.(-1r) * x.|| by CLVECT_1:3
    .= |.-1r.| * ||.x.|| by Th43
    .= |.1r.| * ||.x.|| by COMPLEX1:52;
  hence thesis by COMPLEX1:48;
end;

theorem Th48:
  ||.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 Th46;
  hence thesis by XREAL_1:20;
end;

theorem
  abs(||.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 Th46;
  then ||.y.|| - ||.x.|| <= ||.y - x.|| by XREAL_1:20;
  then ||.y.|| - ||.x.|| <= ||.-(x - y).|| by RLVECT_1:33;
  then ||.y.|| - ||.x.|| <= ||.x - y.|| by Th47;
  then
A1: -(||.x - y.||) <= -(||.y.|| - ||.x.||) by XREAL_1:24;
  ||.x.|| - ||.y.|| <= ||.x - y.|| by Th48;
  hence thesis by A1,ABSVALUE:5;
end;

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

definition
  let X, x, y;
  redefine func dist(x,y);
  commutativity
proof let x,y;
  thus dist(x,y) = ||.-(y-x).|| by RLVECT_1:33
    .= dist(y,x) by Th47;
end;
end;

theorem Th50:
  dist(x,x) = 0
proof
  thus dist(x,x) = ||.09(X).|| by RLVECT_1:15
    .= 0 by Th42;
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 Th46;
end;

theorem Th52:
  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,Th42;
    hence contradiction by A1,RLVECT_1:21;
  end;
  thus thesis by Th50;
end;

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

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 Th52;
    hence thesis by Th44;
  end;
  thus thesis by Th50;
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 Th46;
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 Th46;
  hence thesis by Th47;
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 Th46;
  hence thesis by Th47;
end;

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

definition
  let X, seq1, seq2;
  redefine func seq1 + seq2;
  commutativity
proof let seq1, seq2;
  now
    let n;
    thus (seq1 + seq2).n = seq2.n + seq1.n by NORMSP_1:def 2
      .= (seq2 + seq1).n by NORMSP_1:def 2;
  end;
  hence thesis by FUNCT_2:63;
end;
end;

theorem
  seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3
proof
  now
    let n;
    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;
  hence thesis by FUNCT_2:63;
end;

theorem
  seq1 is constant & seq2 is constant & seq = seq1 + seq2 implies seq is
  constant
proof
  assume that
A1: seq1 is constant and
A2: seq2 is constant and
A3: seq = seq1 + seq2;
  consider x such that
A4: for n being Nat holds seq1.n = x by A1,VALUED_0:def 18;
  consider y such that
A5: for n being Nat holds seq2.n = y by A2,VALUED_0:def 18;
  take z = x + y;
  let n be Nat;
  n in NAT by ORDINAL1:def 12;
  hence seq.n = seq1.n + seq2.n by A3,NORMSP_1:def 2
    .= x + seq2.n by A4
    .= z by A5;
end;

theorem
  seq1 is constant & seq2 is constant & seq = seq1 - seq2 implies seq is
  constant
proof
  assume that
A1: seq1 is constant and
A2: seq2 is constant and
A3: seq = seq1 - seq2;
  consider x such that
A4: for n being Nat holds seq1.n = x by A1,VALUED_0:def 18;
  consider y such that
A5: for n being Nat holds seq2.n = y by A2,VALUED_0:def 18;
  take z = x - y;
  let n be Nat;
  n in NAT by ORDINAL1:def 12;
  hence seq.n = seq1.n - seq2.n by A3,NORMSP_1:def 3
    .= x - seq2.n by A4
    .= z by A5;
end;

theorem
  seq1 is constant & seq = a * seq1 implies seq is constant
proof
  assume that
A1: seq1 is constant and
A2: seq = a * seq1;
  consider x such that
A3: for n being Nat holds seq1.n = x by A1,VALUED_0:def 18;
  take z = a * x;
  let n be Nat;
  n in NAT by ORDINAL1:def 12;
  hence seq.n = a * seq1.n by A2,CLVECT_1:def 14
    .= z by A3;
end;

theorem
  seq1 - seq2 = seq1 + -seq2
proof
  now
    let n;
    thus (seq1 - seq2).n = seq1.n - seq2.n by NORMSP_1:def 3
      .= seq1.n + (-seq2).n by BHSP_1:44
      .= (seq1 + -seq2).n by NORMSP_1:def 2;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  seq = seq + 0.X
proof
  now
    let n;
    thus (seq + 09(X)).n = seq.n + 09(X) by BHSP_1:def 6
      .= seq.n by RLVECT_1:4;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  a * (seq1 + seq2) = a * seq1 + a * seq2
proof
  now
    let n;
    thus (a * (seq1 + seq2)).n = a * (seq1 + seq2).n by CLVECT_1:def 14
      .= a * (seq1.n + seq2.n) by NORMSP_1:def 2
      .= a * seq1.n + a * seq2.n by CLVECT_1:def 2
      .= (a * seq1).n + a * seq2.n by CLVECT_1:def 14
      .= (a * seq1).n + (a * seq2).n by CLVECT_1:def 14
      .= (a * seq1 + a * seq2).n by NORMSP_1:def 2;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  (a + b) * seq = a * seq + b * seq
proof
  now
    let n;
    thus ((a + b) * seq).n = (a + b) * seq.n by CLVECT_1:def 14
      .= a * seq.n + b * seq.n by CLVECT_1:def 3
      .= (a * seq).n + b * seq.n by CLVECT_1:def 14
      .= (a * seq).n + (b * seq).n by CLVECT_1:def 14
      .= (a * seq + b * seq).n by NORMSP_1:def 2;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  (a * b) * seq = a * (b * seq)
proof
  now
    let n;
    thus ((a * b) * seq).n = (a * b) * seq.n by CLVECT_1:def 14
      .= a * (b * seq.n) by CLVECT_1:def 4
      .= a * (b * seq).n by CLVECT_1:def 14
      .= (a * (b * seq)).n by CLVECT_1:def 14;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  1r * seq = seq
proof
  now
    let n;
    thus (1r * seq).n = 1r * seq.n by CLVECT_1:def 14
      .= seq.n by CLVECT_1:def 5;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  (-1r) * seq = - seq
proof
  now
    let n;
    thus ((-1r) * seq).n = (-1r) * seq.n by CLVECT_1:def 14
      .= - seq.n by CLVECT_1:3
      .= (-seq).n by BHSP_1:44;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  seq - x = seq + -x
proof
  now
    let n;
    thus (seq - x).n = seq.n - x by NORMSP_1:def 4
      .= (seq + -x).n by BHSP_1:def 6;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  seq1 - seq2 = - (seq2 - seq1)
proof
  now
    let n;
    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 BHSP_1:44;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  seq = seq - 0.X
proof
  now
    let n;
    thus (seq - 09(X)).n = seq.n - 09(X) by NORMSP_1:def 4
      .= seq.n by RLVECT_1:13;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  seq = - ( - seq )
proof
  now
    let n;
    thus (- ( - seq )).n = - (- seq).n by BHSP_1:44
      .= - ( - seq.n) by BHSP_1:44
      .= seq.n by RLVECT_1:17;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
proof
  now
    let n;
    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;
  hence thesis by FUNCT_2:63;
end;

theorem
  (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3)
proof
  now
    let n;
    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;
  hence thesis by FUNCT_2:63;
end;

theorem
  seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
proof
  now
    let n;
    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;
  hence thesis by FUNCT_2:63;
end;

theorem
  a * (seq1 - seq2) = a * seq1 - a * seq2
proof
  now
    let n;
    thus (a * (seq1 - seq2)).n = a * (seq1 - seq2).n by CLVECT_1:def 14
      .= a * (seq1.n - seq2.n) by NORMSP_1:def 3
      .= a * seq1.n - a * seq2.n by CLVECT_1:9
      .= (a * seq1).n - a * seq2.n by CLVECT_1:def 14
      .= (a * seq1).n - (a * seq2).n by CLVECT_1:def 14
      .= (a * seq1 - a * seq2).n by NORMSP_1:def 3;
  end;
  hence thesis by FUNCT_2:63;
end;

begin :: Complex unitary space of complex sequence

definition
  func cl_scalar -> Function of [:the_set_of_l2ComplexSequences,
  the_set_of_l2ComplexSequences:], COMPLEX means
  for x,y be set st x in
the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds it.(x,
  y) = Sum(seq_id(x)(#)(seq_id(y))*');
  existence
proof
  deffunc F(set,set) = Sum(seq_id($1)(#)(seq_id($2))*');
  set X = the_set_of_l2ComplexSequences;
A1: for x,y being set st x in X & y in X holds F(x,y) in COMPLEX;
  ex f being Function of [:X,X:],COMPLEX st for x,y being set st x in X &
  y in X holds f.(x,y) = F(x,y) from BINOP_1:sch 2(A1);
  hence thesis;
end;
  uniqueness
  proof
    set X = the_set_of_l2ComplexSequences;
    let scalar1, scalar2 be Function of [: X, X :], COMPLEX such that
A2: for x,y be set st x in X & y in X holds scalar1.(x,y) = Sum(seq_id
    (x)(#)(seq_id(y))*') and
A3: for x,y be set st x in X & y in X holds scalar2.(x,y) = Sum(seq_id
    (x)(#)(seq_id(y))*');
    for x, y be set st x in X & y in X holds scalar1.(x,y) = scalar2.(x,y)
    proof
      let x,y be set such that
A4:   x in X and
A5:   y in X;
      thus scalar1.(x,y) = Sum(seq_id(x)(#)(seq_id(y))*') by A2,A4,A5
        .= scalar2.(x,y) by A3,A4,A5;
    end;
    hence thesis by BINOP_1:1;
  end;
end;

registration
  cluster CUNITSTR (# the_set_of_l2ComplexSequences, Zero_(
      the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Add_(
      the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Mult_(
the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), cl_scalar #)
    -> non empty;
  coherence by Def11;
end;

definition
  func Complex_l2_Space -> non empty CUNITSTR equals
  CUNITSTR (#
    the_set_of_l2ComplexSequences, Zero_(the_set_of_l2ComplexSequences,
    Linear_Space_of_ComplexSequences), Add_(the_set_of_l2ComplexSequences,
    Linear_Space_of_ComplexSequences), Mult_(the_set_of_l2ComplexSequences,
    Linear_Space_of_ComplexSequences), cl_scalar #);
  correctness;
end;

theorem Th79:
  for l be CLSStruct st the CLSStruct of l is ComplexLinearSpace
  holds l is ComplexLinearSpace
proof
  let l be CLSStruct such that
A1: the CLSStruct of l is ComplexLinearSpace;
  reconsider l as non empty CLSStruct by A1;
  reconsider l0=CLSStruct (# the carrier of l, 0.l, the addF of l, the Mult of
    l #) as ComplexLinearSpace by A1;
A2: l is Abelian
  proof
    let v,w be VECTOR of l;
    reconsider v1=v as VECTOR of l0;
    reconsider w1=w as VECTOR of l0;
    thus v+w =v1+w1 .= w1+v1
      .= w +v;
  end;
A3: l is add-associative
  proof
    let u,v,w be VECTOR of l;
    reconsider u1=u as VECTOR of l0;
    reconsider v1=v as VECTOR of l0;
    reconsider w1=w as VECTOR of l0;
    thus (u + v) + w = (u1+v1)+w1 .= u1+(v1+w1) by RLVECT_1:def 3
      .= u+(v+w);
  end;
A4: l is vector-distributive scalar-distributive scalar-associative
scalar-unital
  proof
    thus for z being Complex, v,w being VECTOR of l holds z * (v + w) = z * v
    + z * w
    proof
      let z be Complex;
      let v,w be VECTOR of l;
      reconsider v1=v, w1=w as VECTOR of l0;
      thus z*(v+w) =z*(v1+w1) .=z*v1+z*w1 by CLVECT_1:def 2
        .= z*v +z*w;
    end;
    thus for z1,z2 being Complex, v being VECTOR of l holds (z1 + z2) * v = z1
    * v + z2 * v
    proof
      let z1,z2 be Complex;
      let v be VECTOR of l;
      reconsider v1=v as VECTOR of l0;
      thus (z1+z2)*v =(z1+z2)*v1 .=z1*v1+z2*v1 by CLVECT_1:def 3
        .= z1*v +z2*v;
    end;
    thus for z1,z2 being Complex, v being VECTOR of l holds (z1 * z2) * v = z1
    * (z2 * v)
    proof
      let z1,z2 be Complex;
      let v be VECTOR of l;
      reconsider v1=v as VECTOR of l0;
      thus (z1*z2)*v =(z1*z2)*v1 .=z1*(z2*v1) by CLVECT_1:def 4
        .= z1*(z2*v);
    end;
    let v be VECTOR of l;
    reconsider v1=v as VECTOR of l0;
    thus 1r*v= 1r*v1 .= v by CLVECT_1:def 5;
  end;
A5: l is right_complementable
  proof
    let v be VECTOR of l;
    reconsider v1=v as VECTOR of l0;
    consider w1 being VECTOR of l0 such that
A6: v1 + w1 = 0.l0 by ALGSTR_0:def 11;
    reconsider w = w1 as VECTOR of l;
    take w;
    thus thesis by A6;
  end;
  l is right_zeroed
  proof
    let v be VECTOR of l;
    reconsider v1=v as VECTOR of l0;
    thus v+0.l= v1 + 0.l0 .= v by RLVECT_1:def 4;
  end;
  hence thesis by A2,A3,A5,A4;
end;

theorem
  for seq be Complex_Sequence st (for n be Element of NAT holds seq.n=0c
  ) holds seq is summable & Sum seq = 0c
proof
  let seq be Complex_Sequence such that
A1: for n be Element of NAT holds seq.n=0c;
A2: for m be Element of NAT holds Partial_Sums (seq).m = 0c
  proof
    defpred P[Element of NAT] means seq.$1 = (Partial_Sums seq).$1;
    let m be Element of NAT;
A3: for k be Element of NAT st P[k] holds P[k+1]
    proof
      let k be Element of NAT such that
A4:   seq.k = (Partial_Sums (seq)).k;
      thus seq.(k+1) = 0c + (seq).(k+1) .= seq.k + seq.(k+1) by A1
        .= (Partial_Sums seq).(k+1) by A4,SERIES_1:def 1;
    end;
A5: P[0] by SERIES_1:def 1;
    for n be Element of NAT holds P[n] from NAT_1:sch 1(A5,A3);
    hence (Partial_Sums (seq)).m = seq.m .= 0c by A1;
  end;
A6: for p be Real st 0<p ex n be Element of NAT st for m be Element of NAT
  st n<=m holds |.((Partial_Sums seq).m-0c).|<p
  proof
    let p be Real such that
A7: 0<p;
    take 0;
    let m be Element of NAT such that
    0<=m;
    thus thesis by A2,A7,COMPLEX1:44;
  end;
  then
A8: Partial_Sums (seq) qua Complex_Sequence is convergent by COMSEQ_2:def 5;
  then lim (Partial_Sums (seq)) = 0c by A6,COMSEQ_2:def 6;
  hence thesis by A8,COMSEQ_3:def 7,def 8;
end;

registration
  cluster Complex_l2_Space -> Abelian add-associative right_zeroed
    right_complementable vector-distributive scalar-distributive
    scalar-associative scalar-unital;
  coherence by Th14,Th79;
end;