:: Hahn Banach Theorem in the Vector Space over the Field of
:: Complex Numbers
::  by Anna Justyna Milewska
::
:: Received May 23, 2000
:: Copyright (c) 2000-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 RLVECT_1, ALGSTR_0, VECTSP_1, XBOOLE_0, SUBSET_1, RELAT_1,
      ARYTM_1, ARYTM_3, SUPINF_2, XCMPLX_0, COMPLEX1, NUMBERS, CARD_1,
      SQUARE_1, COMPLFLD, GROUP_1, REAL_1, STRUCT_0, HAHNBAN, FUNCT_1,
      FUNCOP_1, MSSUBFAM, UNIALG_1, BINOP_1, LATTICES, MESFUNC1, ZFMISC_1,
      XXREAL_0, RLSUB_1, TARSKI, REALSET1, POWER, HAHNBAN1, FUNCT_7, NAT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, REALSET1, NUMBERS,
      XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, SQUARE_1, POWER, STRUCT_0,
      ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, RLSUB_1, VECTSP_4, FUNCT_1,
      FUNCT_2, BINOP_1, RELSET_1, NATTRA_1, FUNCOP_1, FUNCT_3, HAHNBAN,
      COMPLFLD, XXREAL_0, GRCAT_1;
 constructors REAL_1, SQUARE_1, NAT_1, BINOP_2, POWER, REALSET1, RLSUB_1,
      COMPLFLD, VECTSP_4, NATTRA_1, BORSUK_1, HAHNBAN, SUPINF_1, FUNCOP_1,
      GRCAT_1;
 registrations XBOOLE_0, FUNCT_1, RELSET_1, NUMBERS, XCMPLX_0, XREAL_0,
      MEMBERED, STRUCT_0, RLVECT_1, VECTSP_1, COMPLFLD, HAHNBAN, ALGSTR_0,
      SQUARE_1;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, RLSUB_1, HAHNBAN, RLVECT_1, VECTSP_1, ALGSTR_0;
 equalities SQUARE_1, BINOP_1, RLVECT_1, VECTSP_1, COMPLEX1, STRUCT_0,
      ALGSTR_0;
 expansions TARSKI, VECTSP_1;
 theorems TARSKI, ZFMISC_1, ABSVALUE, FUNCT_1, FUNCT_2, COMPLEX1, COMPLFLD,
      VECTSP_1, FUNCOP_1, RLVECT_1, BINOP_1, HAHNBAN, VECTSP_4, XBOOLE_0,
      RELAT_1, XCMPLX_1, GROUP_1, XXREAL_0, XCMPLX_0, POWER, ALGSTR_0, XREAL_0;
 schemes FUNCT_2, BINOP_1, NAT_1;

begin :: Preliminaries

Lm1: for F be add-associative right_zeroed right_complementable Abelian
right-distributive non empty doubleLoopStr for x,y be Element of F holds x*(-
y) = -x*y
proof
  let F be add-associative right_zeroed right_complementable Abelian
  right-distributive non empty doubleLoopStr;
  let x,y be Element of F;
  x*y +x*(-y) = x*(y+(-y)) by VECTSP_1:def 2
    .= x*(0.F) by RLVECT_1:def 10
    .= 0.F;
  hence thesis by RLVECT_1:def 10;
end;

::$CT

theorem
  for x1,y1,x2,y2 being Real holds (x1+y1*<i>) * (x2+y2*<i>) = x1
  *x2-y1*y2 + (x1*y2+x2*y1)*<i>;

theorem Th2:
  for z be Element of COMPLEX holds |.z.|+0*<i> = (z*'/(|.z.|+0*<i> ))*z
proof
  let z be Element of COMPLEX;
  per cases;
  suppose
A1: |.z.| = 0;
    then z = 0 by COMPLEX1:45;
    hence thesis by A1;
  end;
  suppose
A2: |.z.| <> 0;
A3: Im(z*z*') = 0 by COMPLEX1:40;
    |.z.| = |.z.|+0*<i>;
    then
A4: Re |.z.| = |.z.| & Im |.z.| = 0 by COMPLEX1:12;
A5: (z*'/|.z.|)*z = z*z*'/|.z.| & Re(z*z*') = (Re z)^2 + (Im z)^2 by
COMPLEX1:40,XCMPLX_1:74;
    then
A6: Im((z*'/|.z.|)*z) = (|.z.|*0 - ((Re z)^2+(Im z)^2)*0) / (|.z.| ^2 +0^2
    ) by A3,A4,COMPLEX1:24;
    Re((z*'/|.z.|)*z) = (((Re z)^2+(Im z)^2)*|.z.| + 0*0) / (|.z .|^2 +0^2
    ) by A5,A3,A4,COMPLEX1:24
      .= |.z*z.|*|.z.| / (|.z.|*|.z.|) by COMPLEX1:68
      .= |.z*z.| / |.z.| by A2,XCMPLX_1:91
      .= |.z.|*|.z.| / |.z.| by COMPLEX1:65
      .= |.z.| by A2,XCMPLX_1:89;
    hence thesis by A6,COMPLEX1:13;
  end;
end;

begin :: Some Facts on the Field of Complex Numbers

definition
  let x,y be Real;
  func [**x,y**] -> Element of F_Complex equals
  x+y*<i>;
  coherence
  proof
    x+y*<i> in COMPLEX by XCMPLX_0:def 2;
    hence thesis by COMPLFLD:def 1;
  end;
end;

definition
  func i_FC -> Element of F_Complex equals
  <i>;
  coherence
  proof
    0+1*<i> = [**0,1**];
    hence thesis;
  end;
end;

theorem Th3:
  i_FC * i_FC = -1_F_Complex
proof
  thus i_FC * i_FC = -1r .= -1_F_Complex by COMPLFLD:2,8;
end;

theorem Th4:
  (-1_F_Complex) * (-1_F_Complex) = 1_F_Complex
proof
  -1r = -1_F_Complex by COMPLFLD:2,8;
  hence thesis by COMPLFLD:8;
end;

theorem
  for x1,y1,x2,y2 be Real holds [**x1,y1**] + [**x2,y2**] = [**x1 + x2,
  y1 + y2**];

theorem
  for x1,y1,x2,y2 be Real holds [**x1,y1**] * [**x2,y2**] = [**x1
  *x2 - y1*y2,x1*y2+x2*y1**];

::$CT

theorem
  for r be Real holds |.[**r,0**].| = |.r.|;

theorem
  for x,y be Element of F_Complex holds Re (x+y) = Re x + Re y & Im (x+y
  ) = Im x + Im y by COMPLEX1:8;

theorem
  for x,y be Element of F_Complex holds Re (x*y) = Re x * Re y - Im x *
  Im y & Im (x*y) = Re x * Im y + Re y * Im x by COMPLEX1:9;

begin :: Functionals of Vector Space

definition
  let K be 1-sorted;
  let V be ModuleStr over K;
  mode Functional of V is Function of the carrier of V, the carrier of K;
end;

definition
  let K be non empty addLoopStr;
  let V be non empty ModuleStr over K;
  let f,g be Functional of V;

  func f+g -> Functional of V means
  :Def3:
  for x be Element of V holds it.x = f.x + g.x;
  existence
  proof
    deffunc G(Element of V) = f.$1 + g.$1;
    consider F be Function of the carrier of V,the carrier of K such that
A1: for x be Element of V holds F.x = G(x)from FUNCT_2:sch 4;
    reconsider F as Functional of V;
    take F;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let a,b be Functional of V such that
A2: for x be Element of V holds a.x = f.x + g.x and
A3: for x be Element of V holds b.x = f.x + g.x;
    now
      let x be Element of V;
      thus a.x = f.x + g.x by A2
        .= b.x by A3;
    end;
    hence a = b by FUNCT_2:63;
  end;
end;

definition
  let K be non empty addLoopStr;
  let V be non empty ModuleStr over K;
  let f be Functional of V;
  func -f -> Functional of V means
  :Def4:
  for x be Element of V holds it.x = - (f.x);
  existence
  proof
    deffunc G(Element of V) = -(f.$1);
    consider F be Function of the carrier of V,the carrier of K such that
A1: for x be Element of V holds F.x = G(x) from FUNCT_2:sch 4;
    reconsider F as Functional of V;
    take F;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let a,b be Functional of V such that
A2: for x be Element of V holds a.x = -(f.x) and
A3: for x be Element of V holds b.x = -(f.x);
    now
      let x be Element of V;
      thus a.x = -(f.x) by A2
        .= b.x by A3;
    end;
    hence a = b by FUNCT_2:63;
  end;
end;

definition
  let K be non empty addLoopStr;
  let V be non empty ModuleStr over K;
  let f,g be Functional of V;
  func f-g -> Functional of V equals
  f+-g;
  coherence;
end;

definition
  let K be non empty multMagma;
  let V be non empty ModuleStr over K;
  let v be Element of K;
  let f be Functional of V;
  func v*f -> Functional of V means
  :Def6:
  for x be Element of V holds it.x = v*(f.x);
  existence
  proof
    deffunc G(Element of V) = v *(f.$1);
    consider F be Function of the carrier of V,the carrier of K such that
A1: for x be Element of V holds F.x = G(x) from FUNCT_2:sch 4;
    reconsider F as Functional of V;
    take F;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let a,b be Functional of V such that
A2: for x be Element of V holds a.x = v*(f.x) and
A3: for x be Element of V holds b.x = v*(f.x);
    now
      let x be Element of V;
      thus a.x = v*(f.x) by A2
        .= b.x by A3;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

definition
  let K be non empty ZeroStr;
  let V be ModuleStr over K;
  func 0Functional(V) -> Functional of V equals
  [#]V --> 0.K;
  coherence;
end;

definition
  let K be non empty multMagma;
  let V be non empty ModuleStr over K;
  let F be Functional of V;

  attr F is homogeneous means
  :Def8:
  for x be Vector of V, r be Scalar of V holds F.(r*x) = r*F.x;
end;

definition
  let K be non empty ZeroStr;
  let V be non empty ModuleStr over K;
  let F be Functional of V;
  attr F is 0-preserving means
  F.(0.V) = 0.K;
end;

registration
  let K be add-associative right_zeroed right_complementable Abelian
  associative well-unital distributive non empty doubleLoopStr;
  let V be VectSp of K;
  cluster homogeneous -> 0-preserving for Functional of V;
  coherence
  proof
    let F be Functional of V;
    assume
A1: F is homogeneous;
    thus F.(0.V) = F.(0.K * 0.V) by VECTSP_1:14
      .= 0.K * F.(0.V) by A1
      .= 0.K;
  end;
end;

registration
  let K be right_zeroed non empty addLoopStr;
  let V be non empty ModuleStr over K;
  cluster 0Functional(V) -> additive;
  coherence
  proof
    let x,y be Vector of V;
A1: (0Functional(V)).x = 0.K & (0Functional(V)).y = 0.K by FUNCOP_1:7;
    thus (0Functional(V)).(x+y) = 0.K by FUNCOP_1:7
      .= (0Functional(V)).x + (0Functional(V)).y by A1,RLVECT_1:def 4;
  end;
end;

registration
  let K be add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  cluster 0Functional(V) -> homogeneous;
  coherence
  proof
    let x be Vector of V;
    let r be Scalar of V;
A1: (0Functional(V)).x = 0.K by FUNCOP_1:7;
    thus (0Functional(V)).(r*x) = 0.K by FUNCOP_1:7
      .= r*(0Functional(V)).x by A1;
  end;
end;

registration
  let K be non empty ZeroStr;
  let V be non empty ModuleStr over K;
  cluster 0Functional(V) -> 0-preserving;
  coherence
  by FUNCOP_1:7;
end;

registration
  let K be add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  cluster additive homogeneous 0-preserving for Functional of V;
  existence
  proof
    take 0Functional(V);
    thus thesis;
  end;
end;

theorem Th10:
  for K be Abelian non empty addLoopStr for V be non empty
  ModuleStr over K for f,g be Functional of V holds f+g = g+f
proof
  let K be Abelian non empty addLoopStr;
  let V be non empty ModuleStr over K;
  let f,g be Functional of V;
  now
    let x be Element of V;
    thus (f+g).x = f.x + g.x by Def3
      .= (g+f).x by Def3;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th11:
  for K be add-associative non empty addLoopStr for V be non
  empty ModuleStr over K for f,g,h be Functional of V holds f+g+h = f+(g+h)
proof
  let K be add-associative non empty addLoopStr;
  let V be non empty ModuleStr over K;
  let f,g,h be Functional of V;
  now
    let x be Element of V;
    thus (f+g+h).x = (f+g).x + h.x by Def3
      .= f.x + g.x + h.x by Def3
      .= f.x + (g.x + h.x) by RLVECT_1:def 3
      .= f.x + ((g+h).x) by Def3
      .= (f+(g+h)).x by Def3;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  for K be non empty ZeroStr for V be non empty ModuleStr over K for x
  be Element of V holds (0Functional(V)).x = 0.K by FUNCOP_1:7;

theorem Th13:
  for K be right_zeroed non empty addLoopStr for V be non empty
  ModuleStr over K for f be Functional of V holds f + 0Functional(V) = f
proof
  let K be right_zeroed non empty addLoopStr;
  let V be non empty ModuleStr over K;
  let f be Functional of V;
  now
    let x be Element of V;
    thus (f+0Functional(V)).x = f.x+(0Functional(V)).x by Def3
      .= f.x+0.K by FUNCOP_1:7
      .= f.x by RLVECT_1:def 4;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th14:
  for K be add-associative right_zeroed right_complementable non
empty addLoopStr for V be non empty ModuleStr over K for f be Functional of V
  holds f-f = 0Functional(V)
proof
  let K be add-associative right_zeroed right_complementable non empty
  addLoopStr;
  let V be non empty ModuleStr over K;
  let f be Functional of V;
  now
    let x be Element of V;
    thus (f-f).x = f.x+(-f).x by Def3
      .= f.x+-f.x by Def4
      .= 0.K by RLVECT_1:5
      .= (0Functional(V)).x by FUNCOP_1:7;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th15:
  for K be right-distributive non empty doubleLoopStr for V be
  non empty ModuleStr over K for r be Element of K for f,g be Functional of V
  holds r*(f+g) = r*f+r*g
proof
  let K be right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  let r be Element of K;
  let f,g be Functional of V;
  now
    let x be Element of V;
    thus (r*(f+g)).x = r*(f+g).x by Def6
      .= r*(f.x+g.x) by Def3
      .= r*f.x+r*g.x by VECTSP_1:def 2
      .= (r*f).x+r*g.x by Def6
      .= (r*f).x+(r*g).x by Def6
      .= (r*f+r*g).x by Def3;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th16:
  for K be left-distributive non empty doubleLoopStr for V be
  non empty ModuleStr over K for r,s be Element of K for f be Functional of V
  holds (r+s)*f = r*f+s*f
proof
  let K be left-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  let r,s be Element of K;
  let f be Functional of V;
  now
    let x be Element of V;
    thus ((r+s)*f).x = (r+s)*f.x by Def6
      .= r*f.x+s*f.x by VECTSP_1:def 3
      .= (r*f).x+s*f.x by Def6
      .= (r*f).x+(s*f).x by Def6
      .= (r*f+s*f).x by Def3;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th17:
  for K be associative non empty multMagma for V be non empty
ModuleStr over K for r,s be Element of K for f be Functional of V holds (r*s)*f
  = r*(s*f)
proof
  let K be associative non empty multMagma;
  let V be non empty ModuleStr over K;
  let r,s be Element of K;
  let f be Functional of V;
  now
    let x be Element of V;
    thus ((r*s)*f).x = (r*s)*f.x by Def6
      .= r*(s*f.x) by GROUP_1:def 3
      .= r*(s*f).x by Def6
      .= (r*(s*f)).x by Def6;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th18:
  for K be left_unital non empty doubleLoopStr for V be non
  empty ModuleStr over K for f be Functional of V holds (1.K)*f = f
proof
  let K be left_unital non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  let f be Functional of V;
  now
    let x be Element of V;
    thus ((1.K)*f).x = (1.K)*f.x by Def6
      .= f.x by VECTSP_1:def 8;
  end;
  hence thesis by FUNCT_2:63;
end;

registration
  let K be Abelian add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  let f,g be additive Functional of V;
  cluster f+g -> additive;
  coherence
  proof
    let x,y be Vector of V;
    thus (f+g).(x+y) = f.(x+y)+g.(x+y) by Def3
      .= f.x+f.y+g.(x+y) by VECTSP_1:def 20
      .= f.x+f.y+(g.x+g.y) by VECTSP_1:def 20
      .= f.x+(f.y+(g.x+g.y)) by RLVECT_1:def 3
      .= f.x+(g.x+(f.y+g.y)) by RLVECT_1:def 3
      .= f.x+g.x+(f.y+g.y) by RLVECT_1:def 3
      .= (f+g).x+(f.y+g.y) by Def3
      .= (f+g).x+(f+g).y by Def3;
  end;
end;

registration
  let K be Abelian add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  let f be additive Functional of V;
  cluster -f -> additive;
  coherence
  proof
    let x,y be Vector of V;
    thus (-f).(x+y) = -f.(x+y) by Def4
      .= -(f.x + f.y) by VECTSP_1:def 20
      .= -f.x+-f.y by RLVECT_1:31
      .= (-f).x+-f.y by Def4
      .= (-f).x+(-f).y by Def4;
  end;
end;

registration
  let K be add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  let v be Element of K;
  let f be additive Functional of V;
  cluster v*f -> additive;
  coherence
  proof
    let x,y be Vector of V;
    thus (v*f).(x+y) = v*f.(x+y) by Def6
      .= v*(f.x + f.y) by VECTSP_1:def 20
      .= v*f.x+v*f.y by VECTSP_1:def 2
      .= (v*f).x+v*f.y by Def6
      .= (v*f).x+(v*f).y by Def6;
  end;
end;

registration
  let K be add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  let f,g be homogeneous Functional of V;
  cluster f+g -> homogeneous;
  coherence
  proof
    let x be Vector of V;
    let r be Scalar of V;
    thus (f+g).(r*x) = f.(r*x) + g.(r*x) by Def3
      .= r*f.x + g.(r*x) by Def8
      .= r*f.x + r*g.x by Def8
      .= r*(f.x + g.x) by VECTSP_1:def 2
      .= r*(f+g).x by Def3;
  end;
end;

registration
  let K be Abelian add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  let f be homogeneous Functional of V;
  cluster -f -> homogeneous;
  coherence
  proof
    let x be Vector of V;
    let r be Scalar of V;
    thus (-f).(r*x) = -f.(r*x) by Def4
      .= -r*f.x by Def8
      .= r*-f.x by Lm1
      .= r*(-f).x by Def4;
  end;
end;

registration
  let K be add-associative right_zeroed right_complementable
  right-distributive associative commutative non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  let v be Element of K;
  let f be homogeneous Functional of V;
  cluster v*f -> homogeneous;
  coherence
  proof
    let x be Vector of V;
    let r be Scalar of V;
    thus (v*f).(r*x) = v*f.(r*x) by Def6
      .= v*(r*f.x) by Def8
      .= r*(v*f.x) by GROUP_1:def 3
      .= r*(v*f).x by Def6;
  end;
end;

definition
  let K be add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  mode linear-Functional of V is additive homogeneous Functional of V;
end;

begin :: The Vector Space of linear Functionals

definition
  let K be Abelian add-associative right_zeroed right_complementable
  right-distributive associative commutative non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  func V*' -> non empty strict ModuleStr over K means
  :Def10:
  (for x be set
  holds x in the carrier of it iff x is linear-Functional of V) & (for f,g be
linear-Functional of V holds (the addF of it).(f,g) = f+g) & 0.it = 0Functional
(V) & for f be linear-Functional of V for x be Element of K holds (the lmult of
  it).(x,f) = x*f;
  existence
  proof
    defpred P[set,set,set] means ex f,g be Functional of V st $1=f & $2=g & $3
    =f+g;
    0Functional(V) in the set of all x where x is linear-Functional of V;
    then reconsider
    ca = the set of all x where x is linear-Functional of V
    as non empty set;
A1: now
      let x be set;
      thus x in ca implies x is linear-Functional of V
      proof
        assume x in ca;
        then ex y be linear-Functional of V st x=y;
        hence thesis;
      end;
      thus x is linear-Functional of V implies x in ca;
    end;
    then reconsider 0F=0Functional(V) as Element of ca;
A2: for x,y be Element of ca ex u be Element of ca st P[x,y,u]
    proof
      let x,y be Element of ca;
      reconsider f=x,g=y as linear-Functional of V by A1;
      reconsider u=f+g as Element of ca by A1;
      take u,f,g;
      thus thesis;
    end;
    consider ad be Function of [:ca,ca:],ca such that
A3: for x,y be Element of ca holds P[x,y,ad.(x,y)] from BINOP_1:sch 3(
    A2);
    defpred P[Element of K,set,set] means ex f be Functional of V st $2=f & $3
    =$1*f;
A4: for x be Element of K,y be Element of ca ex u be Element of ca st P[x, y,u]
    proof
      let x be Element of K,y be Element of ca;
      reconsider f=y as linear-Functional of V by A1;
      reconsider u=x*f as Element of ca by A1;
      take u,f;
      thus thesis;
    end;
    consider lm be Function of [:the carrier of K,ca:],ca such that
A5: for x be Element of K,y be Element of ca holds P[x,y,lm.(x,y)]
    from BINOP_1:sch 3(A4);
A6: now
      let f be linear-Functional of V;
      reconsider y=f as Element of ca by A1;
      let x be Element of K;
      ex f1 be Functional of V st y=f1 & lm.(x,y)=x*f1 by A5;
      hence lm.(x,f) = x*f;
    end;
    reconsider V1 = ModuleStr(# ca,ad,0F,lm #) as non empty strict ModuleStr
    over K;
    take V1;
    now
      let f,g be linear-Functional of V;
      reconsider x=f,y=g as Element of ca by A1;
      ex f1,g1 be Functional of V st x=f1 & y=g1 & ad.(x,y)=f1 +g1 by A3;
      hence ad.(f,g) = f+g;
    end;
    hence thesis by A1,A6;
  end;
  uniqueness
  proof
    let V1,V2 be non empty strict ModuleStr over K;
    assume that
A7: for x be set holds x in the carrier of V1 iff x is
    linear-Functional of V and
A8: for f,g be linear-Functional of V holds (the addF of V1).(f,g)=f+ g and
A9: 0.V1 = 0Functional(V) and
A10: for f be linear-Functional of V for x be Element of K holds (the
    lmult of V1).(x,f) = x*f and
A11: for x be set holds x in the carrier of V2 iff x is
    linear-Functional of V and
A12: for f,g be linear-Functional of V holds (the addF of V2).(f,g)=f+ g and
A13: 0.V2 = 0Functional(V) and
A14: for f be linear-Functional of V for x be Element of K holds (the
    lmult of V2).(x,f) = x*f;
A15: now
      let r be Element of K;
      let x be Element of V1;
      reconsider f=x as linear-Functional of V by A7;
      thus (the lmult of V1).(r,x) = r*f by A10
        .= (the lmult of V2).(r,x) by A14;
    end;
    now
      let x be object;
      thus x in the carrier of V1 implies x in the carrier of V2
      proof
        assume x in the carrier of V1;
        then x is linear-Functional of V by A7;
        hence thesis by A11;
      end;
      assume x in the carrier of V2;
      then x is linear-Functional of V by A11;
      hence x in the carrier of V1 by A7;
    end;
    then
A16: the carrier of V1 = the carrier of V2 by TARSKI:2;
    now
      let x,y be Element of V1;
      reconsider f=x, g=y as linear-Functional of V by A7;
      thus (the addF of V1).(x,y) = f+g by A8
        .= (the addF of V2).(x,y) by A12;
    end;
    then the addF of V1 = the addF of V2 by A16,BINOP_1:2;
    hence thesis by A9,A13,A16,A15,BINOP_1:2;
  end;
end;

registration
  let K be Abelian add-associative right_zeroed right_complementable
  right-distributive associative commutative non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  cluster V*' -> Abelian;
  coherence
  proof
    let v,w be Element of V*';
    reconsider f=v,g=w as linear-Functional of V by Def10;
    thus v+w = f+g by Def10
      .= g+f by Th10
      .= w+v by Def10;
  end;
end;

registration
  let K be Abelian add-associative right_zeroed right_complementable
  right-distributive associative commutative non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  cluster V*' -> add-associative;
  coherence
  proof
    let u,v,w be Element of V*';
    reconsider f=u,g=v,h=w as linear-Functional of V by Def10;
    thus u+v+w = (the addF of V*').(f+g,w) by Def10
      .= f+g+h by Def10
      .= f+(g+h) by Th11
      .= (the addF of V*').(u,g+h) by Def10
      .= u+(v+w) by Def10;
  end;
  cluster V*' -> right_zeroed;
  coherence
  proof
    let x be Element of V*';
    reconsider f=x as linear-Functional of V by Def10;
    thus x + 0.(V*') = (the addF of V*').(x,0Functional(V)) by Def10
      .= f+0Functional(V) by Def10
      .= x by Th13;
  end;
  cluster V*' -> right_complementable;
  coherence
  proof
    let x be Element of V*';
    reconsider f=x as linear-Functional of V by Def10;
    reconsider b = -f as Element of V*' by Def10;
    take b;
    thus x+b = f-f by Def10
      .= 0Functional(V) by Th14
      .= 0.(V*') by Def10;
  end;
end;

registration
  let K be Abelian add-associative right_zeroed right_complementable
  left_unital distributive associative commutative non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  cluster V*' -> vector-distributive scalar-distributive
  scalar-associative scalar-unital;
  coherence
  proof
   now let x,y be Element of K;
    let v,w be Element of V*';
    reconsider f=v,g=w as linear-Functional of V by Def10;
    thus x*(v+w) = (the lmult of V*').(x,f+g) by Def10
      .= x*(f+g) by Def10
      .= x*f+x*g by Th15
      .= (the addF of V*').(x*f,x*g) by Def10
      .= (the addF of V*').((the lmult of V*').(x,f),x*g) by Def10
      .= x*v+x*w by Def10;
    thus (x+y)*v = (x+y)*f by Def10
      .= x*f+y*f by Th16
      .= (the addF of V*').(x*f,y*f) by Def10
      .= (the addF of V*').((the lmult of V*').(x,f),y*f) by Def10
      .= x*v+y*v by Def10;
    thus (x*y)*v = (x*y)*f by Def10
      .= x*(y*f) by Th17
      .= (the lmult of V*').(x,y*f) by Def10
      .= x*(y*v) by Def10;
    thus (1.K)*v = (1.K)*f by Def10
      .= v by Th18;
   end;
   hence thesis;
  end;
end;

begin :: Semi Norm of Vector Space

definition
  let K be 1-sorted;
  let V be ModuleStr over K;
  mode RFunctional of V is Function of the carrier of V,REAL;
end;

definition
  let K be 1-sorted;
  let V be non empty ModuleStr over K;
  let F be RFunctional of V;

  attr F is subadditive means
  :Def11:
  for x,y be Vector of V holds F.(x+y) <= F.x+F.y;
end;

definition
  let K be 1-sorted;
  let V be non empty ModuleStr over K;
  let F be RFunctional of V;
  attr F is additive means
  :Def12:
  for x,y be Vector of V holds F.(x+y) = F.x+ F.y;
end;

definition
  let V be non empty ModuleStr over F_Complex;
  let F be RFunctional of V;
  attr F is Real_homogeneous means
  :Def13:
  for v be Vector of V for r be Real holds F.([**r,0**]*v) = r*F.v;
end;

theorem Th19:
  for V be vector-distributive scalar-distributive scalar-associative
  scalar-unital non empty ModuleStr over F_Complex for F
be RFunctional of V st F is Real_homogeneous for v be Vector of V for r be Real
  holds F.([**0,r**]*v) = r*F.(i_FC*v)
proof
  let V be vector-distributive scalar-distributive scalar-associative
  scalar-unital non empty ModuleStr over F_Complex;
  let F be RFunctional of V;
  assume
A1: F is Real_homogeneous;
  let v be Vector of V;
  let r be Real;
  thus F.([**0,r**]*v) = F.([**r,0**]*i_FC*v)
    .= F.([**r,0**]*(i_FC*v)) by VECTSP_1:def 16
    .= r*F.(i_FC*v) by A1;
end;

definition
  let V be non empty ModuleStr over F_Complex;
  let F be RFunctional of V;
  attr F is homogeneous means
  :Def14:
  for v be Vector of V for r be Scalar of V holds F.(r*v) = |.r.|*F.v;
end;

definition
  let K be 1-sorted;
  let V be ModuleStr over K;
  let F be RFunctional of V;
  attr F is 0-preserving means
  F.(0.V) = 0;
end;

registration
  let K be 1-sorted;
  let V be non empty ModuleStr over K;
  cluster additive -> subadditive for RFunctional of V;
  coherence;
end;

registration
  let V be VectSp of F_Complex;
  cluster Real_homogeneous -> 0-preserving for RFunctional of V;
  coherence
  proof
    let F be RFunctional of V;
    assume
A1: F is Real_homogeneous;
A2: 0.F_Complex = [**0,0**] by COMPLFLD:7;
    thus F.(0.V) = F.(0.F_Complex*0.V) by VECTSP_1:14
      .= 0*F.(0.V) by A1,A2
      .= 0;
  end;
end;

definition
  let K be 1-sorted;
  let V be ModuleStr over K;
  func 0RFunctional(V) -> RFunctional of V equals
  [#]V --> 0;
  coherence
   proof
    [#]V --> In(0,REAL) is RFunctional of V;
    hence thesis;
   end;
end;

registration
  let K be 1-sorted;
  let V be non empty ModuleStr over K;
  cluster 0RFunctional(V) -> additive;
  coherence
  proof
    let x,y be Vector of V;
    (0RFunctional(V)).x = 0 & (0RFunctional(V)).y = 0 by FUNCOP_1:7;
    hence thesis by FUNCOP_1:7;
  end;
  cluster 0RFunctional(V) -> 0-preserving;
  coherence
  by FUNCOP_1:7;
end;

registration
  let V be non empty ModuleStr over F_Complex;
  cluster 0RFunctional(V) -> Real_homogeneous;
  coherence
  proof
    let x be Vector of V;
    let r be Real;
    (0RFunctional(V)).x = 0 by FUNCOP_1:7;
    hence thesis by FUNCOP_1:7;
  end;
  cluster 0RFunctional(V) -> homogeneous;
  coherence
  proof
    let x be Vector of V;
    let r be Scalar of V;
    (0RFunctional(V)).x = 0 by FUNCOP_1:7;
    hence thesis by FUNCOP_1:7;
  end;
end;

registration
  let K be 1-sorted;
  let V be non empty ModuleStr over K;
  cluster additive 0-preserving for RFunctional of V;
  existence
  proof
    take 0RFunctional(V);
    thus thesis;
  end;
end;

registration
  let V be non empty ModuleStr over F_Complex;
  cluster additive Real_homogeneous homogeneous for RFunctional of V;
  existence
  proof
    take 0RFunctional(V);
    thus thesis;
  end;
end;

definition
  let V be non empty ModuleStr over F_Complex;
  mode Semi-Norm of V is subadditive homogeneous RFunctional of V;
end;

begin :: Hahn Banach Theorem

definition
  let V be non empty ModuleStr over F_Complex;
  func RealVS(V) -> strict RLSStruct means
  :Def17:
  the addLoopStr of it = the addLoopStr of V &
  for r be Real, v be Vector of V holds (the Mult of it).(r,v)=
  [**r,0**]*v;
  existence
  proof
    deffunc F(Element of REAL, Element of V) = [**$1,0**]*$2;
    consider f be Function of [:REAL, the carrier of V:], the carrier of V
    such that
A1: for r be Element of REAL,
     v be Vector of V holds f.(r,v)=F(r,v) from BINOP_1:
    sch 4;
    take R = RLSStruct (#the carrier of V, 0.V, the addF of V, f#);
    thus the addLoopStr of R = the addLoopStr of V;
    let r be Real;
    let v be Vector of V;
     reconsider r as Element of REAL by XREAL_0:def 1;
     f.(r,v)=F(r,v) by A1;
    hence thesis;
  end;
  uniqueness
  proof
    let a,b be strict RLSStruct such that
A2: the addLoopStr of a = the addLoopStr of V and
A3: for r be Real, v be Vector of V
     holds (the Mult of a).(r,v)=[**r,0**]*v and
A4: the addLoopStr of b = the addLoopStr of V and
A5: for r be Real, v be Vector of V
     holds (the Mult of b).(r,v)=[**r,0 **]*v;
    now
      let r be Element of REAL, v be Vector of V;
      thus (the Mult of a).(r,v) = [**r,0**]*v by A3
        .= (the Mult of b).(r,v) by A5;
    end;
    hence thesis by A2,A4,BINOP_1:2;
  end;
end;

registration
  let V be non empty ModuleStr over F_Complex;
  cluster RealVS(V) -> non empty;
  coherence
  proof
    the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    hence thesis;
  end;
end;

registration
  let V be Abelian non empty ModuleStr over F_Complex;
  cluster RealVS(V) -> Abelian;
  coherence
  proof
    let v,w be Element of RealVS(V);
A1: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider v1=v,w1=w as Element of V;
    thus v + w = v1 + w1 by A1
      .= w1 + v1
      .= w + v by A1;
  end;
end;

registration
  let V be add-associative non empty ModuleStr over F_Complex;
  cluster RealVS(V) -> add-associative;
  coherence
  proof
    let u,v,w be Element of RealVS(V);
A1: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider u1=u,v1=v,w1=w as Element of V;
    thus (u + v) + w = (u1 + v1) + w1 by A1
      .= u1 + (v1 + w1) by RLVECT_1:def 3
      .= u + (v + w) by A1;
  end;
end;

registration
  let V be right_zeroed non empty ModuleStr over F_Complex;
  cluster RealVS(V) -> right_zeroed;
  coherence
  proof
    let v be Element of RealVS(V);
A1: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider v1=v as Element of V;
    thus v + 0.RealVS(V) = v1 + 0.V by A1
      .= v by RLVECT_1:def 4;
  end;
end;

registration
  let V be right_complementable non empty ModuleStr over F_Complex;
  cluster RealVS(V) -> right_complementable;
  coherence
  proof
    let v be Element of RealVS(V);
A1: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider v1=v as Element of V;
    consider w1 be Element of V such that
A2: v1 + w1 = 0.V by ALGSTR_0:def 11;
    reconsider w=w1 as Element of RealVS(V) by A1;
    take w;
    thus thesis by A1,A2;
  end;
end;

registration
  let V be vector-distributive scalar-distributive scalar-associative
  scalar-unital non empty ModuleStr over F_Complex;
  cluster RealVS(V) -> vector-distributive scalar-distributive
  scalar-associative scalar-unital;
  coherence
  proof
    thus for a be Real for v,w be Element of RealVS(V) holds a * (v + w
    ) = a * v + a * w
    proof
      let a be Real;
      reconsider a as Real;
      let v,w be Element of RealVS(V);
      set a1=[**a,0**];
A1:   the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
      then reconsider v1=v,w1=w as Element of V;
      a * (v + w) = [**a,0**] * (v1 + w1) by A1,Def17
        .= a1 * v1 + a1 * w1 by VECTSP_1:def 14
        .= (the addF of V).[((the Mult of RealVS(V)).(a,v1)),[**a,0**]*w1]
      by Def17
        .= a * v + a * w by A1,Def17;
      hence thesis;
    end;
    thus for a,b be Real for v be Element of RealVS(V) holds (a + b) *
    v = a * v + b * v
    proof
      let a,b be Real;
      reconsider a,b as Real;
      let v be Element of RealVS(V);
      set a1=[**a,0**];
      set b1=[**b,0**];
A2:   the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
      then reconsider v1=v as Element of V;
      [**a,0**] + [**b,0**] = [**a+b,0**];
      then (a + b) * v = ([**a,0**] + [**b,0**]) * v1 by Def17
        .= a1 * v1 + b1 * v1 by VECTSP_1:def 15
        .= (the addF of RealVS(V)).[((the Mult of RealVS(V)).(a,v)), ([**b,0
      **]*v1)] by A2,Def17
        .= a * v + b * v by Def17;
      hence thesis;
    end;
    thus for a,b be Real for v be Element of RealVS(V) holds (a * b) *
    v = a * (b * v)
    proof
      let a,b be Real;
      reconsider a,b as Real;
      let v be Element of RealVS(V);
      the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
      then reconsider v1=v as Element of V;
      [**a*b,0**] = [**a,0**]*[**b,0**];
      then (a * b) * v = ([**a,0**] * [**b,0**]) * v1 by Def17
        .= [**a,0**] * ([**b,0**] * v1) by VECTSP_1:def 16
        .= (the Mult of RealVS(V)).(a,([**b,0**] * v1)) by Def17
        .= a * (b * v) by Def17;
      hence thesis;
    end;
    let v be Element of RealVS(V);
    the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider v1=v as Element of V;
    thus 1 * v = [**1,0**] * v1 by Def17
      .= v by COMPLFLD:8,VECTSP_1:def 17;
  end;
end;

theorem Th20:
  for V be non empty VectSp of F_Complex for M be Subspace of V
  holds RealVS(M) is Subspace of RealVS(V)
proof
  let V be non empty VectSp of F_Complex;
  let M be Subspace of V;
A1: the carrier of M c= the carrier of V by VECTSP_4:def 2;
A2: the lmult of M = (the lmult of V) | [:the carrier of F_Complex, the
  carrier of M:] by VECTSP_4:def 2;
A3: the addLoopStr of M = the addLoopStr of RealVS(M) by Def17;
A4: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
  hence
A5: the carrier of RealVS(M) c= the carrier of RealVS(V) by A3,VECTSP_4:def 2;
  then
  [:REAL,the carrier of RealVS(M):] c= [:REAL,the carrier of RealVS(V) :]
  by ZFMISC_1:95;
  then [:REAL,the carrier of RealVS(M):] c= dom (the Mult of RealVS(V)) by
FUNCT_2:def 1;
  then
A6: dom((the Mult of RealVS(V)) | [:REAL,the carrier of RealVS(M):])= [:REAL
  ,the carrier of RealVS(M):] by RELAT_1:62;
  rng ((the Mult of RealVS(V)) | [:REAL,the carrier of RealVS(M):]) c= the
  carrier of RealVS(M)
  proof
    let y be object;
    assume
    y in rng ((the Mult of RealVS(V)) | [:REAL,the carrier of RealVS( M):]);
    then consider x be object such that
A7: x in dom ((the Mult of RealVS(V)) | [:REAL,the carrier of RealVS( M):]) and
A8: y = ((the Mult of RealVS(V)) | [:REAL,the carrier of RealVS(M):])
    .x by FUNCT_1:def 3;
    consider a,b be object such that
A9: x = [a,b] by A7,RELAT_1:def 1;
    reconsider a as Element of REAL by A7,A9,ZFMISC_1:87;
    reconsider b as Element of RealVS(M) by A6,A7,A9,ZFMISC_1:87;
    reconsider b1 = b as Element of M by A3;
    reconsider b2 = b1 as Element of V by A1;
    [[**a,0**],b2] in [:the carrier of F_Complex, the carrier of V:] by
ZFMISC_1:87;
    then [[**a,0**],b1] in [:the carrier of F_Complex, the carrier of M:] & [
    [**a,0 **],b2] in dom (the lmult of V) by FUNCT_2:def 1,ZFMISC_1:87;
    then [[**a,0**],b2] in (dom (the lmult of V)) /\ [:the carrier of
    F_Complex, the carrier of M:] by XBOOLE_0:def 4;
    then
A10: [[**a,0**],b2] in dom ((the lmult of V) | [:the carrier of F_Complex,
    the carrier of M:]) by RELAT_1:61;
    y = (the Mult of RealVS(V)).(a,b) by A7,A8,A9,FUNCT_1:47
      .= [**a,0**]*b2 by Def17
      .= [**a,0**]*b1 by A2,A10,FUNCT_1:47
      .= (the Mult of RealVS(M)).(a,b) by Def17;
    hence thesis;
  end;
  then reconsider
  RM = (the Mult of RealVS(V)) | [: REAL,the carrier of RealVS(M)
:] as Function of [:REAL,the carrier of RealVS(M):],the carrier of RealVS(M)
by A6,FUNCT_2:2;
  thus 0.RealVS(M) = 0.M by A3
    .= 0.V by VECTSP_4:def 2
    .= 0.RealVS(V) by A4;
  thus the addF of RealVS(M) = (the addF of RealVS(V))||the carrier of RealVS(
  M) by A3,A4,VECTSP_4:def 2;
  now
    let a be Element of REAL, b be Element of RealVS(M);
    reconsider b1 = b as Element of M by A3;
    reconsider b2 = b1 as Element of V by A1;
    [[**a,0**],b2] in [:the carrier of F_Complex, the carrier of V:] by
ZFMISC_1:87;
    then [[**a,0**],b1] in [:the carrier of F_Complex, the carrier of M:] & [
    [**a,0 **],b2] in dom (the lmult of V) by FUNCT_2:def 1,ZFMISC_1:87;
    then [[**a,0**],b2] in (dom (the lmult of V)) /\ [:the carrier of
    F_Complex, the carrier of M:] by XBOOLE_0:def 4;
    then
A11: [[**a,0**],b2] in dom ((the lmult of V) | [:the carrier of F_Complex,
    the carrier of M:]) by RELAT_1:61;
    a in REAL & b in the carrier of RealVS(V)
            by A5;
    then [a,b] in [: REAL,the carrier of RealVS(V) :] by ZFMISC_1:87;
    then
    [a,b] in [: REAL,the carrier of RealVS(M) :] & [a,b] in dom (the Mult
    of RealVS(V)) by FUNCT_2:def 1,ZFMISC_1:87;
    then [a,b] in (dom (the Mult of RealVS(V))) /\ [: REAL,the carrier of
    RealVS(M) :] by XBOOLE_0:def 4;
    then
A12: [a,b] in dom RM by RELAT_1:61;
    thus (the Mult of RealVS(M)).(a,b) = [**a,0**]*b1 by Def17
      .= [**a,0**]*b2 by A2,A11,FUNCT_1:47
      .= (the Mult of RealVS(V)).(a,b) by Def17
      .= RM.(a,b) by A12,FUNCT_1:47;
  end;
  hence
  the Mult of RealVS(M) = (the Mult of RealVS(V)) | [:REAL,the carrier of
  RealVS(M):] by BINOP_1:2;
end;

theorem Th21:
  for V be non empty ModuleStr over F_Complex for p be RFunctional
  of V holds p is Functional of RealVS(V)
proof
  let V be non empty ModuleStr over F_Complex;
  let p be RFunctional of V;
  the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
  hence thesis;
end;

theorem Th22:
  for V be non empty VectSp of F_Complex for p be Semi-Norm of V
  holds p is Banach-Functional of RealVS(V)
proof
  let V be non empty VectSp of F_Complex;
  let p be Semi-Norm of V;
  reconsider p1=p as Functional of RealVS(V) by Th21;
A1: p1 is positively_homogeneous
  proof
    let x be VECTOR of RealVS(V);
    let r be Real;
    assume
A2: r > 0;
    the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider x1=x as Vector of V;
    r*x = [**r,0**]*x1 by Def17;
    hence p1.(r*x) = |.r.|*p1.x by Def14
      .= r*p1.x by A2,ABSVALUE:def 1;
  end;
  p1 is subadditive
  proof
    let x,y be VECTOR of RealVS(V);
A3: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider x1=x, y1=y as Vector of V;
    x+y = x1+y1 by A3;
    hence thesis by Def11;
  end;
  hence thesis by A1;
end;

definition
  let V be non empty ModuleStr over F_Complex;
  let l be Functional of V;
  func projRe(l) -> Functional of RealVS(V) means
  :Def18:
  for i be Element of V holds it.i = Re(l.i);
  existence
  proof
    deffunc F(Element of V) = Re(l.$1);
    consider f be Function of the carrier of V,REAL such that
A1: for i be Element of V holds f.i = F(i) from FUNCT_2:sch 4;
    the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider f as Functional of RealVS(V);
    take f;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let a,b be Functional of RealVS(V);
    assume
A2: for i be Element of V holds a.i = Re(l.i);
    assume
A3: for i be Element of V holds b.i = Re(l.i);
    now
      let i be Element of RealVS(V);
      the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
      then reconsider j=i as Element of V;
      thus a.i = Re(l.j) by A2
        .= b.i by A3;
    end;
    hence a = b by FUNCT_2:63;
  end;
end;

definition
  let V be non empty ModuleStr over F_Complex;
  let l be Functional of V;
  func projIm(l) -> Functional of RealVS(V) means
  :Def19:
  for i be Element of V holds it.i = Im(l.i);
  existence
  proof
    deffunc F(Element of V) = Im(l.$1);
    consider f be Function of the carrier of V,REAL such that
A1: for i be Element of V holds f.i = F(i) from FUNCT_2:sch 4;
    the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider f as Functional of RealVS(V);
    take f;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let a,b be Functional of RealVS(V);
    assume
A2: for i be Element of V holds a.i = Im(l.i);
    assume
A3: for i be Element of V holds b.i = Im(l.i);
    now
      let i be Element of RealVS(V);
      the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
      then reconsider j=i as Element of V;
      thus a.i = Im(l.j) by A2
        .= b.i by A3;
    end;
    hence a = b by FUNCT_2:63;
  end;
end;

definition
  let V be non empty ModuleStr over F_Complex;
  let l be Functional of RealVS(V);
  func RtoC(l) -> RFunctional of V equals
  l;
  coherence
  proof
    the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    hence thesis;
  end;
end;

definition
  let V be non empty ModuleStr over F_Complex;
  let l be RFunctional of V;
  func CtoR(l) -> Functional of RealVS(V) equals
  l;
  coherence
  proof
    the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    hence thesis;
  end;
end;

registration
  let V be non empty VectSp of F_Complex;
  let l be additive Functional of RealVS(V);
  cluster RtoC(l) -> additive;
  coherence
  proof
    let x,y be Vector of V;
A1: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider x1=x,y1=y as VECTOR of RealVS(V);
    x+y = x1+y1 by A1;
    hence (RtoC l).(x+y) = (RtoC l).x+(RtoC l).y by HAHNBAN:def 2;
  end;
end;

registration
  let V be non empty VectSp of F_Complex;
  let l be additive RFunctional of V;
  cluster CtoR(l) -> additive;
  coherence
  proof
    let x,y be VECTOR of RealVS(V);
A1: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider x1=x,y1=y as Vector of V;
    x+y = x1+y1 by A1;
    hence thesis by Def12;
  end;
end;

registration
  let V be non empty VectSp of F_Complex;
  let l be homogeneous Functional of RealVS(V);
  cluster RtoC(l) -> Real_homogeneous;
  coherence
  proof
    let x be Vector of V;
    let r be Real;
    the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider x1=x as VECTOR of RealVS(V);
    [**r,0**]*x = r*x1 by Def17;
    hence thesis by HAHNBAN:def 3;
  end;
end;

registration
  let V be non empty VectSp of F_Complex;
  let l be Real_homogeneous RFunctional of V;
  cluster CtoR(l) -> homogeneous;
  coherence
  proof
    let x be VECTOR of RealVS(V);
    let r be Real;
    the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider x1=x as Vector of V;
    reconsider r as Real;
    [**r,0**]*x1 = r*x by Def17;
    hence thesis by Def13;
  end;
end;

definition
  let V be non empty ModuleStr over F_Complex;
  let l be RFunctional of V;
  func i-shift(l) -> RFunctional of V means
  :Def22:
  for v be Element of V holds it.v = l.(i_FC*v);
  existence
  proof
    deffunc F(Element of V) = l.(i_FC*$1);
    consider f be Function of the carrier of V,REAL such that
A1: for v be Element of V holds f.v = F(v) from FUNCT_2:sch 4;
    reconsider f as RFunctional of V;
    take f;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let F1,F2 be RFunctional of V such that
A2: for v be Element of V holds F1.v = l.(i_FC*v) and
A3: for v be Element of V holds F2.v = l.(i_FC*v);
    now
      let v be Element of V;
      thus F1.v = l.(i_FC*v) by A2
        .= F2.v by A3;
    end;
    hence F1 = F2 by FUNCT_2:63;
  end;
end;

definition
  let V be non empty ModuleStr over F_Complex;
  let l be Functional of RealVS(V);
  func prodReIm(l) -> Functional of V means
  :Def23:
  for v be Element of V holds it.v = [**(RtoC l).v,-(i-shift(RtoC l)).v**];
  existence
  proof
    deffunc F(Element of V) = [**(RtoC l).$1,-(i-shift(RtoC l)).$1**];
    consider f be Function of the carrier of V,the carrier of F_Complex such
    that
A1: for v be Element of V holds f.v = F(v) from FUNCT_2:sch 4;
    reconsider f as Functional of V;
    take f;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let a,b be Functional of V;
    assume
A2: for v be Element of V holds a.v = [**(RtoC l).v,-(i-shift(RtoC l)) .v**];
    assume
A3: for v be Element of V holds b.v = [**(RtoC l).v,-(i-shift(RtoC l)) .v**];
    now
      let v be Element of V;
      thus a.v = [**(RtoC l).v,-(i-shift(RtoC l)).v**] by A2
        .= b.v by A3;
    end;
    hence a = b by FUNCT_2:63;
  end;
end;

theorem Th23:
  for V be non empty VectSp of F_Complex for l be
  linear-Functional of V holds projRe(l) is linear-Functional of RealVS(V)
proof
  let V be non empty VectSp of F_Complex;
  let l be linear-Functional of V;
A1: projRe(l) is homogeneous
  proof
    let x be VECTOR of RealVS(V);
    let r be Real;
    the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider x1=x as Vector of V;
    r*x = [**r,0**]*x1 by Def17;
    hence (projRe(l)).(r*x) = Re(l.([**r,0**]*x1)) by Def18
      .= Re([**r,0**]*l.x1) by Def8
      .= Re [**r,0**] * Re (l.x1) - Im [**r,0**] * Im (l.x1) by COMPLEX1:9
      .= Re [**r,0**] * Re (l.x1) - 0 * Im (l.x1) by COMPLEX1:12
      .= r * Re (l.x1) by COMPLEX1:12
      .= r*(projRe(l)).x by Def18;
  end;
  projRe(l) is additive
  proof
    let x,y be VECTOR of RealVS(V);
A2: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider x1=x, y1=y as Vector of V;
    thus (projRe(l)).(x+y) = Re(l.(x1+y1)) by A2,Def18
      .= Re(l.x1+l.y1) by VECTSP_1:def 20
      .= Re(l.x1)+Re(l.y1) by COMPLEX1:8
      .= Re(l.x1)+(projRe(l)).y by Def18
      .= (projRe(l)).x+(projRe(l)).y by Def18;
  end;
  hence thesis by A1;
end;

theorem
  for V be non empty VectSp of F_Complex for l be linear-Functional of V
  holds projIm(l) is linear-Functional of RealVS(V)
proof
  let V be non empty VectSp of F_Complex;
  let l be linear-Functional of V;
A1: projIm(l) is homogeneous
  proof
    let x be VECTOR of RealVS(V);
    let r be Real;
    the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider x1=x as Vector of V;
    r*x = [**r,0**]*x1 by Def17;
    hence (projIm(l)).(r*x) = Im(l.([**r,0**]*x1)) by Def19
      .= Im([**r,0**]*l.x1) by Def8
      .= Re [**r,0**] * Im (l.x1) + Re (l.x1) * Im [**r,0**] by COMPLEX1:9
      .= Re [**r,0**] * Im (l.x1) + Re (l.x1) * 0 by COMPLEX1:12
      .= r * Im (l.x1) by COMPLEX1:12
      .= r*(projIm(l)).x by Def19;
  end;
  projIm(l) is additive
  proof
    let x,y be VECTOR of RealVS(V);
A2: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
    then reconsider x1=x, y1=y as Vector of V;
    thus (projIm(l)).(x+y) = Im(l.(x1+y1)) by A2,Def19
      .= Im(l.x1+l.y1) by VECTSP_1:def 20
      .= Im(l.x1)+Im(l.y1) by COMPLEX1:8
      .= Im(l.x1)+(projIm(l)).y by Def19
      .= (projIm(l)).x+(projIm(l)).y by Def19;
  end;
  hence thesis by A1;
end;

theorem Th25:
  for V be non empty VectSp of F_Complex for l be
  linear-Functional of RealVS(V) holds prodReIm(l) is linear-Functional of V
proof
  let V be non empty VectSp of F_Complex;
  let l be linear-Functional of RealVS(V);
A1: prodReIm(l) is homogeneous
  proof
    let x be Vector of V;
    let r be Scalar of V;
    reconsider r1=r as Element of COMPLEX by COMPLFLD:def 1;
    set a=Re r1,b=Im r1;
A2: r1 = a+b*<i> by COMPLEX1:13;
A3: -1_F_Complex = [**-1,0**] by COMPLFLD:2,8;
    x = i_FC*(i_FC*(-1_F_Complex))*x by Th3,Th4,VECTSP_1:def 17
      .= i_FC*((-1_F_Complex)*i_FC*x) by VECTSP_1:def 16;
    then
A4: a*(-(RtoC l).(i_FC*x))+((RtoC l).x)*b = -a*(RtoC l).(i_FC*x)+b*(RtoC l
    ).(i_FC*((-1_F_Complex)*i_FC*x))
      .= -(RtoC l).([**a,0**]*(i_FC*x))+ -(-b)*(RtoC l).(i_FC*((-1_F_Complex
    )*i_FC*x)) by Def13
      .= -(RtoC l).([**a,0**]*(i_FC*x))+ -(RtoC l).([**0,-b**]*((-
    1_F_Complex)*i_FC*x)) by Th19
      .= -(RtoC l).([**a,0**]*(i_FC*x))+ -(RtoC l).([**0,-b**]*((-
    1_F_Complex)*(i_FC*x))) by VECTSP_1:def 16
      .= -(RtoC l).([**a,0**]*(i_FC*x))+ -(RtoC l).([**0,-b**]*(-1_F_Complex
    )*(i_FC*x)) by VECTSP_1:def 16
      .= -((RtoC l).([**a,0**]*(i_FC*x))+(RtoC l).([**0,b**]*(i_FC*x))) by A3
      .= -(RtoC l).([**a,0**]*(i_FC*x)+[**0,b**]*(i_FC*x)) by Def12
      .= -(RtoC l).(([**a,0**]+[**0,b**])*(i_FC*x)) by VECTSP_1:def 15
      .= -(RtoC l).(i_FC*r*x) by A2,VECTSP_1:def 16;
A5: a*((RtoC l).x)-b*(-(RtoC l).(i_FC*x)) = a*((RtoC l).x)+b*(RtoC l).( i_FC*x)
      .= (RtoC l).([**a,0**]*x)+b*(RtoC l).(i_FC*x) by Def13
      .= (RtoC l).([**a,0**]*x)+(RtoC l).([**0,b**]*x) by Th19
      .= (RtoC l).([**a,0**]*x+[**0,b**]*x) by Def12
      .= (RtoC l).(([**a,0**]+[**0,b**])*x) by VECTSP_1:def 15
      .= (RtoC l).(r*x) by COMPLEX1:13;
    thus (prodReIm(l)).(r*x) = [**(RtoC l).(r*x),-(i-shift(RtoC l)).(r*x)**]
    by Def23
      .= [**(RtoC l).(r*x),-(RtoC l).(i_FC*(r*x))**] by Def22
      .= (RtoC l).(r*x)+(a*(-(RtoC l).(i_FC*x))+((RtoC l).x)*b)*<i> by A4,
VECTSP_1:def 16
      .= r*[**(RtoC l).x,-(RtoC l).(i_FC*x)**] by A2,A5
      .= r*[**(RtoC l).x,-(i-shift(RtoC l)).x**] by Def22
      .= r*(prodReIm(l)).x by Def23;
  end;
  prodReIm(l) is additive
  proof
    let x,y be Vector of V;
    thus (prodReIm(l)).(x+y) = [**(RtoC l).(x+y),-(i-shift(RtoC l)).(x+y)**]
    by Def23
      .= [**(RtoC l).(x+y),-(RtoC l).(i_FC*(x+y))**] by Def22
      .= [**(RtoC l).x+(RtoC l).y,-(RtoC l).(i_FC*(x+y))**] by Def12
      .= [**(RtoC l).x+(RtoC l).y, -(RtoC l).(i_FC*x+i_FC*y)**] by
VECTSP_1:def 14
      .= [**(RtoC l).x+(RtoC l).y, -((RtoC l).(i_FC*x)+(RtoC l).(i_FC*y))**]
    by Def12
      .= [**(RtoC l).x,-(RtoC l).(i_FC*x)**] + [**(RtoC l).y,-(RtoC l).(i_FC
    *y)**]
      .= [**(RtoC l).x,-(i-shift(RtoC l)).x**] + [**(RtoC l).y,-(RtoC l).(
    i_FC*y)**] by Def22
      .= [**(RtoC l).x,-(i-shift(RtoC l)).x**] + [**(RtoC l).y,-(i-shift(
    RtoC l)).y**] by Def22
      .= (prodReIm(l)).x + [**(RtoC l).y,-(i-shift(RtoC l)).y**] by Def23
      .= (prodReIm(l)).x + (prodReIm(l)).y by Def23;
  end;
  hence thesis by A1;
end;

:: Hahn Banach Theorem

::$N Hahn-Banach Theorem  (complex spaces)
theorem
  for V be non empty VectSp of F_Complex for p be Semi-Norm of V for M
be Subspace of V for l be linear-Functional of M st for e be Vector of M for v
be Vector of V st v=e holds |.l.e.| <= p.v ex L be linear-Functional of V st L|
  the carrier of M = l & for e be Vector of V holds |.L.e.| <= p.e
proof
  let V be non empty VectSp of F_Complex;
  let p be Semi-Norm of V;
  reconsider p1=p as Banach-Functional of RealVS(V) by Th22;
  let M be Subspace of V;
  reconsider tcM = the carrier of M as Subset of V by VECTSP_4:def 2;
  reconsider RVSM = RealVS(M) as Subspace of RealVS(V) by Th20;
  let l be linear-Functional of M;
  reconsider prRl = projRe(l) as linear-Functional of RVSM by Th23;
A1: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
A2: the addLoopStr of M = the addLoopStr of RealVS(M) by Def17;
  assume
A3: for e be Vector of M for v be Vector of V st v=e holds |.l.e.| <= p. v;
  for x be VECTOR of RVSM for v be VECTOR of RealVS(V) st x=v holds prRl.x
  <= p1.v
  proof
    let x be VECTOR of RVSM;
    reconsider x1=x as Vector of M by A2;
    let v be VECTOR of RealVS(V);
    reconsider v1=v as Vector of V by A1;
    prRl.x = Re(l.x1) by Def18;
    then
A4: prRl.x <= |.l.x1.| by COMPLEX1:54;
    assume x=v;
    then |.l.x1.| <= p.v1 by A3;
    hence thesis by A4,XXREAL_0:2;
  end;
  then consider L1 be linear-Functional of RealVS(V) such that
A5: L1|the carrier of RVSM=prRl and
A6: for e be VECTOR of RealVS(V) holds L1.e <= p1.e by HAHNBAN:22;
  reconsider L=prodReIm(L1) as linear-Functional of V by Th25;
  take L;
  now
    let x be Element of M;
    the carrier of M c= the carrier of V by VECTSP_4:def 2;
    then reconsider x2=x as Element of V;
    reconsider x1=x2,ix1=i_FC*x2 as Element of RealVS(V) by A1;
    reconsider lx=l.x as Element of COMPLEX by COMPLFLD:def 1;
    lx = Re lx+(Im lx)*<i> by COMPLEX1:13;
    then
A7: i_FC*l.x = 0*Re lx-1*Im lx + (0*Im lx+1*Re lx)*<i>;
A8: i_FC*x = i_FC*x2 by VECTSP_4:14;
    then
A9: L1.ix1 = (projRe(l)).ix1 by A2,A5,FUNCT_1:49
      .= Re(l.(i_FC*x)) by A8,Def18
      .= Re((-Im lx)+Re lx*<i>) by A7,Def8
      .= -Im(l.x) by COMPLEX1:12;
A10: L1.x1 = (projRe(l)).x1 by A2,A5,FUNCT_1:49
      .= Re(l.x) by Def18;
    thus (L|tcM).x = L.x by FUNCT_1:49
      .= [**(RtoC L1).x2,-(i-shift(RtoC L1)).x2**] by Def23
      .= [**Re(l.x),-(RtoC L1).(i_FC*x2)**] by A10,Def22
      .= l.x by A9,COMPLEX1:13;
  end;
  hence L|the carrier of M = l by FUNCT_2:63;
  let e be Vector of V;
  reconsider Le = L.e as Element of COMPLEX by COMPLFLD:def 1;
  Le*'/|.Le.| in COMPLEX by XCMPLX_0:def 2;
  then reconsider Ledz = Le*'/|.Le.| as Element of F_Complex
          by COMPLFLD:def 1;
  reconsider e1=e,Ledze=Ledz*e as VECTOR of RealVS(V) by A1;
  per cases;
  suppose
A11: |.Le.| <> 0;
A12: |.Ledz.| = |.Le*'.|/|.|.Le.|.| by COMPLEX1:67
      .= |.Le.|/|.Le.| by COMPLEX1:53
      .= 1 by A11,XCMPLX_1:60;
    |.Le.|+0*<i> = Ledz*L.e by Th2
      .= L.(Ledz*e) by Def8
      .= [**(RtoC L1).(Ledz*e),-(i-shift(RtoC L1)).(Ledz*e)**] by Def23
      .= L1.Ledze+(-(i-shift(RtoC L1)).(Ledz*e))*<i>;
    then
A13: L1.Ledze = |.L.e.| by COMPLEX1:77;
    p1.Ledze = |.Ledz.|*p.e by Def14
      .= p.e by A12;
    hence thesis by A6,A13;
  end;
  suppose
A14: |.Le.| = 0;
    |.L.e.| = |.[**(RtoC L1).e,-(i-shift(RtoC L1)).e**].| by Def23
      .= |.(RtoC L1).e+(-(i-shift(RtoC L1)).e)*<i>.|;
    then (RtoC L1).e+(-(i-shift(RtoC L1)).e)*<i> = 0+0*<i> by A14,COMPLEX1:45;
    then L1.e1 = 0 by COMPLEX1:77;
    hence thesis by A6,A14;
  end;
end;

begin :: Addenda
:: from COMPTRIG, 2006.08.12, A.T.

theorem
  for x be Real st x > 0 for n be Nat holds (power F_Complex)
  .([**x,0**],n) = [**x to_power n,0**]
proof
  let x be Real;
  defpred P[Nat] means
    (power F_Complex).([**x,0**],$1) = [**x to_power $1,0**];
  assume
A1: x > 0;
A2: now
    let n be Nat;
    assume P[n];
    then
    (power F_Complex).([**x,0**],n+1) = [**x to_power n,0**]*[**x,0**] by
GROUP_1:def 7
      .= [**(x to_power n)*(x to_power 1),0**] by POWER:25
      .= [**x to_power (n+1),0**] by A1,POWER:27;
    hence P[n+1];
  end;
  (power F_Complex).([**x,0**],0) = 1r+0*<i> by COMPLFLD:8,GROUP_1:def 7
    .= [**x to_power 0,0**] by POWER:24;
  then
A3: P[0];
  thus for n be Nat holds P[n] from NAT_1:sch 2(A3,A2);
end;