:: Hahn Banach Theorem
::  by Bogdan Nowak and Andrzej Trybulec
::
:: Received July 8, 1993
:: Copyright (c) 1993-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, SUBSET_1, PARTFUN1, FUNCT_1, TARSKI, RELAT_1,
      SUPINF_1, XXREAL_0, ORDINAL1, ARYTM_3, ORDINAL2, XXREAL_2, RLVECT_1,
      RLSUB_1, STRUCT_0, SUPINF_2, RLSUB_2, FINSEQ_4, MCART_1, RLVECT_3,
      REAL_1, CARD_1, MSSUBFAM, UNIALG_1, COMPLEX1, FUNCOP_1, ARYTM_1,
      ALGSTR_0, XREAL_0, REALSET1, ZFMISC_1, NORMSP_1, HAHNBAN, NORMSP_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XXREAL_0, XREAL_0, COMPLEX1, STRUCT_0, ALGSTR_0, REAL_1, RELAT_1,
      REALSET1, FUNCT_1, FUNCT_2, RLVECT_1, RLSUB_1, RLSUB_2, NORMSP_0,
      NORMSP_1, SUPINF_1, PARTFUN1, FUNCOP_1, RLVECT_3, DOMAIN_1, XXREAL_2;
 constructors BINOP_1, REAL_1, COMPLEX1, SUPINF_1, REALSET1, RFUNCT_3, RLSUB_2,
      RLVECT_2, RLVECT_3, NORMSP_1, XXREAL_2, RELSET_1, XXREAL_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, PARTFUN1, NUMBERS, XXREAL_0,
      XREAL_0, MEMBERED, STRUCT_0, RLVECT_1, RLSUB_1, ALGSTR_0, FUNCT_2,
      FUNCT_1, RELAT_1, DOMAIN_1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, RLSUB_1, RLSUB_2, RLVECT_1, ORDINAL1, XBOOLE_0, STRUCT_0,
      ALGSTR_0, XXREAL_2, SUPINF_1;
 theorems PARTFUN1, RLSUB_1, FUNCT_2, ZFMISC_1, FUNCOP_1, TREES_2, TARSKI,
      FUNCT_1, GRFUNC_1, RLVECT_1, RLSUB_2, RLVECT_4, MCART_1, RLVECT_3,
      ABSVALUE, NORMSP_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_0,
      XCMPLX_1, XREAL_1, XXREAL_0, NUMBERS, STRUCT_0, ALGSTR_0, XXREAL_2,
      NORMSP_0;
 schemes ORDERS_1, DOMAIN_1, FUNCT_2;

begin :: Some Facts on Real Vector Spaces

reserve V for RealLinearSpace;

theorem Th1:
  for W1,W2 being Subspace of V holds the carrier of W1 c= the
  carrier of W1 + W2
proof
  let W1,W2 be Subspace of V;
  let x be set;
  assume
A1: x in the carrier of W1;
  the carrier of W1 c= the carrier of V by RLSUB_1:def 2;
  then reconsider w = x as VECTOR of V by A1;
A2: w + 0.V = w & 0.V in W2 by RLSUB_1:17,RLVECT_1:4;
  x in W1 by A1,STRUCT_0:def 5;
  then x in {v + u where v,u is VECTOR of V : v in W1 & u in W2} by A2;
  hence thesis by RLSUB_2:def 1;
end;

theorem Th2:
  for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
for v,v1,v2 being VECTOR of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds v |--
  (W1,W2) = [v1,v2]
proof
  let W1,W2 be Subspace of V;
  assume
A1: V is_the_direct_sum_of W1,W2;
  let v,v1,v2 be VECTOR of V;
  [v1,v2]`1 = v1 & [v1,v2]`2 = v2 by MCART_1:7;
  hence thesis by A1,RLSUB_2:def 6;
end;

theorem Th3:
  for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
  for v,v1,v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds v = v1 + v2
proof
  let W1,W2 be Subspace of V such that
A1: V is_the_direct_sum_of W1,W2;
  let v,v1,v2 be VECTOR of V;
  assume v |-- (W1,W2) = [v1,v2];
  then (v |-- (W1,W2))`1 = v1 & (v |-- (W1,W2))`2 = v2 by MCART_1:7;
  hence thesis by A1,RLSUB_2:def 6;
end;

theorem Th4:
  for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
for v,v1,v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds v1 in W1 & v2 in
  W2
proof
  let W1,W2 be Subspace of V such that
A1: V is_the_direct_sum_of W1,W2;
  let v,v1,v2 be VECTOR of V;
  assume v |-- (W1,W2) = [v1,v2];
  then (v |-- (W1,W2))`1 = v1 & (v |-- (W1,W2))`2 = v2 by MCART_1:7;
  hence thesis by A1,RLSUB_2:def 6;
end;

theorem Th5:
  for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
for v,v1,v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds v |-- (W2,W1) =
  [v2,v1]
proof
  let W1,W2 be Subspace of V;
  assume
A1: V is_the_direct_sum_of W1,W2;
  let v,v1,v2 be VECTOR of V;
  assume
A2: v |-- (W1,W2) = [v1,v2];
  then
A3: (v |-- (W1,W2))`1 = v1 by MCART_1:7;
  then
A4: v1 in W1 by A1,RLSUB_2:def 6;
A5: (v |-- (W1,W2))`2 = v2 by A2,MCART_1:7;
  then
A6: v2 in W2 by A1,RLSUB_2:def 6;
  v = v2 + v1 by A1,A3,A5,RLSUB_2:def 6;
  hence thesis by A1,A4,A6,Th2,RLSUB_2:38;
end;

theorem Th6:
  for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
  for v being VECTOR of V st v in W1 holds v |-- (W1,W2) = [v,0.V]
proof
  let W1,W2 be Subspace of V such that
A1: V is_the_direct_sum_of W1,W2;
  let v be VECTOR of V such that
A2: v in W1;
  0.V in W2 & v + 0.V = v by RLSUB_1:17,RLVECT_1:4;
  hence thesis by A1,A2,Th2;
end;

theorem Th7:
  for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
  for v being VECTOR of V st v in W2 holds v |-- (W1,W2) = [0.V,v]
proof
  let W1,W2 be Subspace of V;
  assume
A1: V is_the_direct_sum_of W1,W2;
  let v be VECTOR of V;
  assume v in W2;
  then v |-- (W2,W1) = [v,0.V] by A1,Th6,RLSUB_2:38;
  hence thesis by A1,Th5,RLSUB_2:38;
end;

theorem Th8:
  for V1 being Subspace of V, W1 being Subspace of V1, v being
  VECTOR of V st v in W1 holds v is VECTOR of V1
proof
  let V1 be Subspace of V, W1 be Subspace of V1, v be VECTOR of V;
  assume v in W1;
  then the carrier of W1 c= the carrier of V1 & v in the carrier of W1 by
RLSUB_1:def 2,STRUCT_0:def 5;
  hence thesis;
end;

theorem Th9:
  for V1,V2,W being Subspace of V, W1,W2 being Subspace of W st W1
  = V1 & W2 = V2 holds W1 + W2 = V1 + V2
proof
  let V1,V2,W be Subspace of V, W1,W2 be Subspace of W such that
A1: W1 = V1 & W2 = V2;
  reconsider W3 = W1 + W2 as Subspace of V by RLSUB_1:27;
  now
    let v be VECTOR of V;
A2: the carrier of W1 c= the carrier of W & the carrier of W2 c= the
    carrier of W by RLSUB_1:def 2;
    hereby
      assume
A3:   v in W3;
      then reconsider w = v as VECTOR of W by Th8;
      consider w1,w2 being VECTOR of W such that
A4:   w1 in W1 & w2 in W2 and
A5:   w = w1 + w2 by A3,RLSUB_2:1;
      reconsider v1 = w1, v2 = w2 as VECTOR of V by RLSUB_1:10;
      v = v1 + v2 by A5,RLSUB_1:13;
      hence v in V1 + V2 by A1,A4,RLSUB_2:1;
    end;
    assume v in V1 + V2;
    then consider v1,v2 being VECTOR of V such that
A6: v1 in V1 & v2 in V2 and
A7: v = v1 + v2 by RLSUB_2:1;
    v1 in the carrier of W1 & v2 in the carrier of W2 by A1,A6,STRUCT_0:def 5;
    then reconsider w1 = v1, w2 = v2 as VECTOR of W by A2;
    v = w1 + w2 by A7,RLSUB_1:13;
    hence v in W3 by A1,A6,RLSUB_2:1;
  end;
  hence thesis by RLSUB_1:31;
end;

theorem Th10:
  for W being Subspace of V for v being VECTOR of V, w being
  VECTOR of W st v = w holds Lin{w} = Lin{v}
proof
  let W be Subspace of V;
  let v be VECTOR of V, w be VECTOR of W such that
A1: v = w;
  reconsider W1 = Lin{w} as Subspace of V by RLSUB_1:27;
  now
    let u be VECTOR of V;
    hereby
      assume u in W1;
      then consider a being Real such that
A2:   u = a * w by RLVECT_4:8;
      u = a * v by A1,A2,RLSUB_1:14;
      hence u in Lin{v} by RLVECT_4:8;
    end;
    assume u in Lin{v};
    then consider a being Real such that
A3: u = a * v by RLVECT_4:8;
    u = a * w by A1,A3,RLSUB_1:14;
    hence u in W1 by RLVECT_4:8;
  end;
  hence thesis by RLSUB_1:31;
end;

theorem Th11:
  for v being VECTOR of V, X being Subspace of V st not v in X for
  y being VECTOR of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & W = X
  holds X + Lin{v} is_the_direct_sum_of W,Lin{y}
proof
  let v be VECTOR of V, X be Subspace of V such that
A1: not v in X;
  let y be VECTOR of X + Lin{v}, W be Subspace of X + Lin{v};
  assume that
A2: v = y and
A3: W = X;
  Lin{v} = Lin{y} by A2,Th10;
  hence the RLSStruct of X + Lin{v} = W + Lin{y} by A3,Th9;
  assume W /\ Lin{y} <> (0).(X + Lin{v});
  then consider z being VECTOR of X + Lin{v} such that
A4: not(z in W /\ Lin{y} iff z in (0).(X + Lin{v})) by RLSUB_1:31;
  per cases by A4;
  suppose that
A5: z in W /\ Lin{y} and
A6: not z in (0).(X + Lin{v});
    z in Lin{y} by A5,RLSUB_2:3;
    then consider a being Real such that
A7: z = a * y by RLVECT_4:8;
A8: z in W by A5,RLSUB_2:3;
    now
      per cases;
      suppose
        a = 0;
        then z = 0.(X + Lin{v}) by A7,RLVECT_1:10;
        hence contradiction by A6,RLSUB_1:17;
      end;
      suppose
A9:     a <> 0;
        y = 1*y by RLVECT_1:def 8
          .= a"*a*y by A9,XCMPLX_0:def 7
          .= a"*(a*y) by RLVECT_1:def 7;
        hence contradiction by A1,A2,A3,A8,A7,RLSUB_1:21;
      end;
    end;
    hence contradiction;
  end;
  suppose that
A10: not z in W /\ Lin{y} and
A11: z in (0).(X + Lin{v});
    z = 0.(X + Lin{v}) by A11,RLVECT_3:29;
    hence contradiction by A10,RLSUB_1:17;
  end;
end;

theorem Th12:
  for v being VECTOR of V, X being Subspace of V, y being VECTOR
  of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & X = W & not v in X
  holds y |-- (W,Lin{y}) = [0.W,y]
proof
  let v be VECTOR of V, X be Subspace of V, y be VECTOR of X + Lin{v}, W be
  Subspace of X + Lin{v};
  assume v = y & X = W & not v in X;
  then X + Lin{v} is_the_direct_sum_of W,Lin{y} by Th11;
  then y |-- (W,Lin{y}) = [0.(X + Lin{v}),y] by Th7,RLVECT_4:9;
  hence thesis by RLSUB_1:11;
end;

theorem Th13:
  for v being VECTOR of V, X being Subspace of V, y being VECTOR
of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & X = W & not v in X for
  w being VECTOR of X + Lin{v} st w in X holds w |-- (W,Lin{y}) = [w,0.V]
proof
  let v be VECTOR of V, X be Subspace of V, y be VECTOR of X + Lin{v}, W be
  Subspace of X + Lin{v} such that
A1: v = y and
A2: X = W and
A3: not v in X;
A4: X + Lin{v} is_the_direct_sum_of W,Lin{y} by A1,A2,A3,Th11;
  let w be VECTOR of X + Lin{v};
  assume w in X;
  then w |-- (W,Lin{y}) = [w,0.(X + Lin{v})] by A2,A4,Th6;
  hence thesis by RLSUB_1:11;
end;

theorem Th14:
  for v being VECTOR of V, W1,W2 being Subspace of V ex v1,v2
  being VECTOR of V st v |-- (W1,W2) = [v1,v2]
proof
  let v be VECTOR of V, W1,W2 be Subspace of V;
  take (v |-- (W1,W2))`1,(v |-- (W1,W2))`2;
  thus thesis by MCART_1:21;
end;

theorem Th15:
  for v being VECTOR of V, X being Subspace of V, y being VECTOR
of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & X = W & not v in X for
w being VECTOR of X + Lin{v} ex x being VECTOR of X, r being Real st w |-- (W,
  Lin{y}) = [x,r*v]
proof
  let v be VECTOR of V, X be Subspace of V, y be VECTOR of X + Lin{v}, W be
  Subspace of X + Lin{v} such that
A1: v = y and
A2: X = W and
A3: not v in X;
  let w be VECTOR of X + Lin{v};
  consider v1,v2 being VECTOR of X + Lin{v} such that
A4: w |-- (W,Lin{y}) = [v1,v2] by Th14;
A5: X + Lin{v} is_the_direct_sum_of W,Lin{y} by A1,A2,A3,Th11;
  then v1 in W by A4,Th4;
  then reconsider x = v1 as VECTOR of X by A2,STRUCT_0:def 5;
  v2 in Lin{y} by A5,A4,Th4;
  then consider r being Real such that
A6: v2 = r * y by RLVECT_4:8;
  take x,r;
  thus thesis by A1,A4,A6,RLSUB_1:14;
end;

theorem Th16:
  for v being VECTOR of V, X being Subspace of V, y being VECTOR
of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & X = W & not v in X for
w1,w2 being VECTOR of X + Lin{v}, x1,x2 being VECTOR of X, r1,r2 being Real st
w1 |-- (W,Lin{y}) = [x1,r1*v] & w2 |-- (W,Lin{y}) = [x2,r2*v] holds w1 + w2 |--
  (W,Lin{y}) = [x1 + x2, (r1+r2)*v]
proof
  let v be VECTOR of V, X be Subspace of V, y be VECTOR of X + Lin{v}, W be
  Subspace of X + Lin{v};
  assume that
A1: v = y and
A2: X = W and
A3: not v in X;
A4: X + Lin{v} is_the_direct_sum_of W,Lin{y} by A1,A2,A3,Th11;
  let w1,w2 be VECTOR of X + Lin{v}, x1,x2 be VECTOR of X, r1,r2 be Real such
  that
A5: w1 |-- (W,Lin{y}) = [x1,r1*v] and
A6: w2 |-- (W,Lin{y}) = [x2,r2*v];
  reconsider y1 = x1, y2 = x2 as VECTOR of X + Lin{v} by A2,RLSUB_1:10;
A7: r2*v = r2*y by A1,RLSUB_1:14;
  then
A8: y2 in W by A4,A6,Th4;
  (r1+r2)*v = (r1+r2)*y by A1,RLSUB_1:14;
  then
A9: (r1+r2)*v in Lin{y} by RLVECT_4:8;
  reconsider z1 = x1, z2 = x2 as VECTOR of V by RLSUB_1:10;
A10: y1 + y2 = z1 + z2 by RLSUB_1:13
    .= x1 + x2 by RLSUB_1:13;
A11: r1*v = r1*y by A1,RLSUB_1:14;
  then y1 in W by A4,A5,Th4;
  then
A12: y1 + y2 in W by A8,RLSUB_1:20;
A13: w2 = y2 + r2*y by A4,A6,A7,Th3;
  w1 = y1 + r1*y by A4,A5,A11,Th3;
  then
A14: w1 + w2 = y1 + r1*y + y2 + r2*y by A13,RLVECT_1:def 3
    .= y1 + y2 + r1*y + r2*y by RLVECT_1:def 3
    .= y1 + y2 + (r1*y + r2*y) by RLVECT_1:def 3
    .= y1 + y2 + (r1+r2)*y by RLVECT_1:def 6;
  (r1+r2)*y = (r1+r2)*v by A1,RLSUB_1:14;
  hence thesis by A4,A12,A9,A14,A10,Th2;
end;

theorem Th17:
  for v being VECTOR of V, X being Subspace of V, y being VECTOR
of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & X = W & not v in X for
w being VECTOR of X + Lin{v}, x being VECTOR of X, t,r being Real st w |-- (W,
  Lin{y}) = [x,r*v] holds t*w |-- (W,Lin{y}) = [t*x, t*r*v]
proof
  let v be VECTOR of V, X be Subspace of V, y be VECTOR of X + Lin{v}, W be
  Subspace of X + Lin{v};
  assume that
A1: v = y and
A2: X = W and
A3: not v in X;
A4: X + Lin{v} is_the_direct_sum_of W,Lin{y} by A1,A2,A3,Th11;
  let w be VECTOR of X + Lin{v}, x be VECTOR of X, t,r be Real such that
A5: w |-- (W,Lin{y}) = [x,r*v];
  reconsider z = x as VECTOR of X + Lin{v} by A2,RLSUB_1:10;
  r*y = r*v by A1,RLSUB_1:14;
  then
A6: t*w = t*(z + r*y) by A4,A5,Th3
    .= t*z + t*(r*y) by RLVECT_1:def 5
    .= t*z + t*r*y by RLVECT_1:def 7;
  reconsider u = x as VECTOR of V by RLSUB_1:10;
A7: t*r*y in Lin{y} by RLVECT_4:8;
A8: t*r*y = t*r*v by A1,RLSUB_1:14;
A9: t*z = t*u by RLSUB_1:14
    .= t*x by RLSUB_1:14;
  then t*z in W by A2,STRUCT_0:def 5;
  hence thesis by A4,A9,A8,A7,A6,Th2;
end;

begin :: Functionals in Real Linear Space

definition
  let V be RLSStruct;
  mode Functional of V is Function of the carrier of V,REAL;
end;

definition
  let V;
  let IT be Functional of V;

  attr IT is subadditive means
  :Def1:
  for x,y being VECTOR of V holds IT.(x+y) <= IT.x+IT.y;
  attr IT is additive means
  :Def2:
  for x,y being VECTOR of V holds IT.(x+y) = IT.x+IT.y;
  attr IT is homogeneous means
  :Def3:
  for x being VECTOR of V, r being Real holds IT.(r*x) = r*IT.x;
  attr IT is positively_homogeneous means
  :Def4:
  for x being VECTOR of V, r being Real st r > 0 holds IT.(r*x) = r*IT.x;
  attr IT is semi-homogeneous means
  :Def5:
  for x being VECTOR of V, r being Real st r >= 0 holds IT.(r*x) = r*IT.x;
  attr IT is absolutely_homogeneous means
  :Def6:
  for x being VECTOR of V, r being Real holds IT.(r*x) = abs(r)*IT.x;
  attr IT is 0-preserving means
  :Def7:
  IT.(0.V) = 0;
end;

registration
  let V;
  cluster additive -> subadditive for Functional of V;
  coherence
  proof
    let f be Functional of V;
    assume
A1: f is additive;
    let x,y be VECTOR of V;
    thus thesis by A1,Def2;
  end;
  cluster homogeneous -> positively_homogeneous for Functional of V;
  coherence
  proof
    let f be Functional of V;
    assume
A2: f is homogeneous;
    let x be VECTOR of V, r be Real;
    thus thesis by A2,Def3;
  end;
  cluster semi-homogeneous -> positively_homogeneous for Functional of V;
  coherence
  proof
    let f be Functional of V;
    assume
A3: f is semi-homogeneous;
    let x be VECTOR of V, r be Real;
    assume r > 0;
    hence thesis by A3,Def5;
  end;
  cluster semi-homogeneous -> 0-preserving for Functional of V;
  coherence
  proof
    let f be Functional of V;
    assume
A4: f is semi-homogeneous;
    thus f.(0.V) = f.(0*0.V) by RLVECT_1:10
      .= 0*f.(0.V) by A4,Def5
      .= 0;
  end;
  cluster absolutely_homogeneous -> semi-homogeneous for Functional of V;
  coherence
  proof
    let f be Functional of V;
    assume
A5: f is absolutely_homogeneous;
    let x be VECTOR of V, r be Real;
    assume r >= 0;
    then abs r = r by ABSVALUE:def 1;
    hence thesis by A5,Def6;
  end;
  cluster 0-preserving positively_homogeneous -> semi-homogeneous for
Functional
    of V;
  coherence
  proof
    let f be Functional of V such that
A6: f is 0-preserving and
A7: f is positively_homogeneous;
    let x be VECTOR of V, r be Real such that
A8: r >= 0;
    per cases by A8;
    suppose
A9:   r = 0;
      hence f.(r*x) = f.(0.V) by RLVECT_1:10
        .= r*f.x by A6,A9,Def7;
    end;
    suppose
      r > 0;
      hence thesis by A7,Def4;
    end;
  end;
end;

registration
  let V;
  cluster additive absolutely_homogeneous homogeneous for Functional of V;
  existence
  proof
    reconsider f = (the carrier of V) --> 0 as Functional of V;
    take f;
    hereby
      let x,y be VECTOR of V;
      thus f.(x+y) = 0+0 by FUNCOP_1:7
        .= f.x+0 by FUNCOP_1:7
        .= f.x+f.y by FUNCOP_1:7;
    end;
    hereby
      let x be VECTOR of V, r be Real;
      thus f.(r*x) = abs(r)*0 by FUNCOP_1:7
        .= abs(r)*f.x by FUNCOP_1:7;
    end;
    let x be VECTOR of V, r be Real;
    thus f.(r*x) = r*0 by FUNCOP_1:7
      .= r*f.x by FUNCOP_1:7;
  end;
end;

definition
  let V;
  mode Banach-Functional of V is subadditive positively_homogeneous Functional
    of V;
  mode linear-Functional of V is additive homogeneous Functional of V;
end;

theorem Th18:
  for L being homogeneous Functional of V, v being VECTOR of V
  holds L.(-v) = - L.v
proof
  let L be homogeneous Functional of V, v be VECTOR of V;
  thus L.(-v) = L.((-1)*v) by RLVECT_1:16
    .= (-1)*L.v by Def3
    .= - L.v;
end;

theorem Th19:
  for L being linear-Functional of V, v1,v2 being VECTOR of V
  holds L.(v1 - v2) = L.v1 - L.v2
proof
  let L be linear-Functional of V, v1,v2 be VECTOR of V;
  thus L.(v1 - v2) = L.(v1) + L.(-v2) by Def2
    .= L.v1 + - L.v2 by Th18
    .= L.v1 - L.v2;
end;

theorem Th20:
  for L being additive Functional of V holds L.(0.V) = 0
proof
  let L be additive Functional of V;
  L.(0.V) + 0 = L.(0.V + 0.V) by RLVECT_1:4
    .= L.(0.V) + L.(0.V) by Def2;
  hence thesis;
end;

theorem Th21:
  for X being Subspace of V, fi being linear-Functional of X, v
  being VECTOR of V, y being VECTOR of X + Lin{v} st v = y & not v in X for r
being Real ex psi being linear-Functional of X + Lin{v} st psi|the carrier of X
  =fi & psi.y = r
proof
  let X be Subspace of V, fi be linear-Functional of X, v be VECTOR of V, y be
  VECTOR of X + Lin{v} such that
A1: v = y and
A2: not v in X;
  reconsider W1 = X as Subspace of X + Lin{v} by RLSUB_2:7;
  let r be Real;
  defpred P[VECTOR of X + Lin{v},Real] means for x being VECTOR of X, s being
Real st ($1 |-- (W1,Lin{y}))`1 = x & ($1 |-- (W1,Lin{y}))`2 = s*v holds $2 = fi
  .x + s*r;
A3: now
    let e be Element of X + Lin{v};
    consider x being VECTOR of X, s being Real such that
A4: e |-- (W1,Lin{y}) = [x,s*v] by A1,A2,Th15;
    take u = fi.x + s*r;
    thus P[e,u]
    proof
      let x9 be VECTOR of X, t be Real such that
A5:   (e |-- (W1,Lin{y}))`1 = x9 and
A6:   (e |-- (W1,Lin{y}))`2 = t*v;
      v <> 0.V by A2,RLSUB_1:17;
      then t = s by A4,A6,MCART_1:7,RLVECT_1:37;
      hence thesis by A4,A5,MCART_1:7;
    end;
  end;
  consider f being Function of the carrier of X + Lin{v},REAL such that
A7: for e being VECTOR of X + Lin{v} holds P[e,f.e] from FUNCT_2:sch 3(
  A3);
A8: now
    let a be set;
    assume a in dom fi;
    then reconsider x = a as VECTOR of X by FUNCT_2:def 1;
    the carrier of X c= the carrier of X + Lin{v} by Th1;
    then reconsider v1 = x as VECTOR of X + Lin{v} by TARSKI:def 3;
    v1 in X by STRUCT_0:def 5;
    then (v1 |-- (W1,Lin{y})) = [v1,0.V] by A1,A2,Th13
      .= [v1,0*v] by RLVECT_1:10;
    then
A9: (v1 |-- (W1,Lin{y}))`1 = x & (v1 |-- (W1,Lin{y}))`2 = 0*v by MCART_1:7;
    thus fi.a = fi.x + 0*r .= f.a by A7,A9;
  end;
  reconsider f as Functional of X + Lin{v};
A10: y |-- (W1,Lin{y}) = [0.W1,y] by A1,A2,Th12;
  then
A11: (y |-- (W1,Lin{y}))`1 = 0.X by MCART_1:7;
A12: f is additive
  proof
    let v1,v2 be VECTOR of X + Lin{v};
    consider x1 being VECTOR of X, s1 being Real such that
A13: v1 |-- (W1,Lin{y}) = [x1,s1*v] by A1,A2,Th15;
A14: (v1 |-- (W1,Lin{y}))`1 = x1 & (v1 |-- (W1,Lin{y}))`2 = s1*v by A13,
MCART_1:7;
    consider x2 being VECTOR of X, s2 being Real such that
A15: v2 |-- (W1,Lin{y}) = [x2,s2*v] by A1,A2,Th15;
A16: (v2 |-- (W1,Lin{y}))`1 = x2 & (v2 |-- (W1,Lin{y}))`2 = s2*v by A15,
MCART_1:7;
    v1 + v2 |-- (W1,Lin{y}) = [x1 +x2,(s1+s2)*v] by A1,A2,A13,A15,Th16;
    then
    (v1 + v2 |-- (W1,Lin{y}))`1 = x1 + x2 & (v1 + v2 |-- (W1,Lin{y}))`2 =
    (s1+ s2)*v by MCART_1:7;
    hence f.(v1+v2) = fi.(x1 + x2) + (s1 + s2)*r by A7
      .= fi.(x1) + fi.(x2) + (s1*r + s2*r) by Def2
      .= fi.(x1) + s1*r + (fi.(x2) + s2*r)
      .= f.v1 + (fi.(x2) + s2*r) by A7,A14
      .= f.v1+f.v2 by A7,A16;
  end;
  f is homogeneous
  proof
    let v0 be VECTOR of X + Lin{v}, t be Real;
    consider x0 being VECTOR of X, s0 being Real such that
A17: v0 |-- (W1,Lin{y}) = [x0,s0*v] by A1,A2,Th15;
A18: (v0 |-- (W1,Lin{y}))`1 = x0 & (v0 |-- (W1,Lin{y}))`2 = s0*v by A17,
MCART_1:7;
    t*v0 |-- (W1,Lin{y}) = [t*x0,t*s0*v] by A1,A2,A17,Th17;
    then (t*v0 |-- (W1,Lin{y}))`1 = t*x0 & (t*v0 |-- (W1,Lin{y}))`2 = t*s0*v
    by MCART_1:7;
    hence f.(t*v0) = fi.(t*x0) + t*s0*r by A7
      .= t*(fi.x0) + t*(s0*r) by Def3
      .= t*(fi.x0 + s0*r)
      .= t*f.v0 by A7,A18;
  end;
  then reconsider f as linear-Functional of X + Lin{v} by A12;
  take f;
  dom fi = the carrier of X & dom f = the carrier of X + Lin{v} by
FUNCT_2:def 1;
  then dom fi = dom f /\ the carrier of X by Th1,XBOOLE_1:28;
  hence f|the carrier of X=fi by A8,FUNCT_1:46;
  (y |-- (W1,Lin{y}))`2 = y by A10,MCART_1:7
    .= 1*v by A1,RLVECT_1:def 8;
  hence f.y = fi.(0.X) + 1*r by A7,A11
    .= 0 + 1*r by Th20
    .= r;
end;

begin :: Hahn Banach Theorem

Lm1: for X being Subspace of V, v being VECTOR of V st not v in the carrier of
X for q being Banach-Functional of V, fi being linear-Functional of X st for x
being VECTOR of X, v being VECTOR of V st x=v holds fi.x <= q.v ex psi being
linear-Functional of X + Lin{v} st psi|the carrier of X=fi & for x being VECTOR
of X + Lin{v}, v being VECTOR of V st x = v holds psi.x <= q.v
proof
  let X be Subspace of V, v be VECTOR of V;
  assume not v in the carrier of X;
  then
A1: not v in X by STRUCT_0:def 5;
  v in Lin{v} by RLVECT_4:9;
  then
A2: v in the carrier of Lin{v} by STRUCT_0:def 5;
  the carrier of Lin{v} c= the carrier of Lin{v} + X by Th1;
  then reconsider x0 = v as VECTOR of X + Lin{v} by A2,RLSUB_2:5;
  set x1 = the VECTOR of X;
  let q be Banach-Functional of V, fi be linear-Functional of X such that
A3: for x being VECTOR of X, v being VECTOR of V st x=v holds fi.x <= q. v;
  set A = { fi.x - q.(y - v) where x is VECTOR of X, y is VECTOR of V : x = y
  }, B = { fi.x + q.(v - y) where x is VECTOR of X, y is VECTOR of V : x = y };
A4: now
    let x1,x2 be VECTOR of X, y1,y2 be VECTOR of V;
    assume x1 = y1 & x2 = y2;
    then fi.(x1 - x2) <= q.(y1 - y2) by A3,RLSUB_1:16;
    then
A5: fi.x1 - fi.x2 <= q.(y1 - y2) by Th19;
    y1 - y2 = y1 + 0.V + -y2 by RLVECT_1:4
      .= y1 + (-v + v) + -y2 by RLVECT_1:5
      .= y1 - v + v + -y2 by RLVECT_1:def 3
      .= y1 - v + (v - y2) by RLVECT_1:def 3;
    then q.(y1 - y2) <= q.(y1 - v) + q.(v - y2) by Def1;
    then fi.x1 - fi.x2 <= q.(v - y2) + q.(y1 - v) by A5,XXREAL_0:2;
    then fi.x1 <= fi.x2 + (q.(v - y2) + q.(y1 - v)) by XREAL_1:20;
    then fi.x1 <= fi.x2 + q.(v - y2) + q.(y1 - v);
    hence fi.x1 - q.(y1 - v) <= fi.x2 + q.(v - y2) by XREAL_1:20;
  end;
A6: now
    let a,b be R_eal;
    assume a in A;
    then
A7: ex x1 being VECTOR of X, y1 being VECTOR of V st a = fi.x1 - q.(y1 - v
    ) & x1 = y1;
    assume b in B;
    then
    ex x2 being VECTOR of X, y2 being VECTOR of V st b = fi.x2 + q.(v - y2
    ) & x2 = y2;
    hence a <= b by A4,A7;
  end;
  reconsider v1 = x1 as VECTOR of V by RLSUB_1:10;
A8: A c= REAL
  proof
    let a be set;
    assume a in A;
    then
    ex x being VECTOR of X, y being VECTOR of V st a = fi.x - q.(y - v) &
    x = y;
    hence thesis;
  end;
A9: B c= REAL
  proof
    let b be set;
    assume b in B;
    then
    ex x being VECTOR of X, y being VECTOR of V st b = fi.x + q.(v - y) &
    x = y;
    hence thesis;
  end;
  fi.x1 - q.(v1 - v) in A & fi.x1 + q.(v - v1) in B;
  then reconsider A, B as non empty Subset of ExtREAL by A8,A9,NUMBERS:31
,XBOOLE_1:1;
A10: sup A <= inf B by A6,XXREAL_2:96;
A11: A is bounded_above
  proof
    set b = the Element of B;
    reconsider b as real number by A9;
    take b;
      let x be ext-real number;
      thus thesis by A6;
  end;
  A <> {-infty}
  proof
    set x = the Element of A;
    assume A = {-infty};
    then x = -infty by TARSKI:def 1;
    hence contradiction by A8;
  end;
  then reconsider r = sup A as Real by A11,XXREAL_2:57;
  consider psi being linear-Functional of X + Lin{v} such that
A12: psi|the carrier of X=fi and
A13: psi.x0 = r by A1,Th21;
  take psi;
  thus psi|the carrier of X=fi by A12;
  let y be VECTOR of X + Lin{v}, u be VECTOR of V such that
A14: y = u;
  y in X + Lin{v} by STRUCT_0:def 5;
  then consider y1,y29 being VECTOR of V such that
A15: y1 in X and
A16: y29 in Lin{v} and
A17: y = y1 + y29 by RLSUB_2:1;
  y1 in X + Lin{v} by A15,RLSUB_2:2;
  then reconsider x = y1 as VECTOR of X + Lin{v} by STRUCT_0:def 5;
  reconsider x1 = x as VECTOR of X by A15,STRUCT_0:def 5;
  consider t being Real such that
A18: y29 = t * v by A16,RLVECT_4:8;
  per cases;
  suppose
    t = 0;
    then y29 = 0.V by A18,RLVECT_1:10;
    then
A19: y = x1 by A17,RLVECT_1:4;
    then fi.x1 <= q.u by A3,A14;
    hence thesis by A12,A19,FUNCT_1:49;
  end;
  suppose
A20: t > 0;
    reconsider b = psi.((-t)"*x) + q.(v - (-t)"*y1) as R_eal by XBOOLE_0:def 3
,XXREAL_0:def 4;
A21: v - (-t)"*y1 = v - (-t")*y1 by XCMPLX_1:222
      .= v + - -t"*y1 by RLVECT_4:3
      .= v + t"*y1 by RLVECT_1:17;
A22: (-t)"*x1 = (-t)"*y1 by RLSUB_1:14;
    then (-t)"*x1 = (-t)"*x by RLSUB_1:14;
    then fi.((-t)"*x1) = psi.((-t)"*x) by A12,FUNCT_1:49;
    then psi.((-t)"*x) + q.(v - (-t)"*y1) in B by A22;
    then inf B <= b by XXREAL_2:3;
    then sup A <= b by A10,XXREAL_0:2;
    then psi.((-t)"*x) >= r - q.(v - (-t)"*y1) by XREAL_1:20;
    then
A23: - psi.((-t)"*x) <= - (r - q.(v - (-t)"*y1)) by XREAL_1:24;
    - psi.((-t)"*x) = (-1)*psi.((-t)"*x) .= psi.((-1)*((-t)"*x)) by Def3
      .= psi.((-1)*(-t)"*x) by RLVECT_1:def 7
      .= psi.((-1)*(-t")*x) by XCMPLX_1:222
      .= psi.(t"*x);
    then
A24: psi.(t"*x) <= q.(v + t"*y1) - r by A23,A21;
    t"*u = t"*y1 + t"*y29 by A14,A17,RLVECT_1:def 5
      .= t"*y1 + t"*t*v by A18,RLVECT_1:def 7
      .= t"*y1 + 1*v by A20,XCMPLX_0:def 7
      .= v + t"*y1 by RLVECT_1:def 8;
    then psi.(t"*x) + r <= q.(t"*u) by A24,XREAL_1:19;
    then
A25: psi.(t"*x) + r <= t"*(q.u) by A20,Def4;
    y29 in X + Lin{v} by A16,RLSUB_2:2;
    then reconsider y2 = y29 as VECTOR of X + Lin{v} by STRUCT_0:def 5;
    y2 = t*x0 by A18,RLSUB_1:14;
    then
A26: y = x + t*x0 by A17,RLSUB_1:13;
A27: t*(t"*(q.u)) = t*t"*(q.u) .= 1*(q.u) by A20,XCMPLX_0:def 7
      .= q.u;
    psi.(x + t*x0) = psi.x + psi.(t*x0) by Def2
      .= 1*(psi.x + t*psi.x0) by Def3
      .= t*t"*(psi.x + t*psi.x0) by A20,XCMPLX_0:def 7
      .= t*(t"*(psi.x) + t"*t*psi.x0)
      .= t*(t"*(psi.x) + 1*psi.x0) by A20,XCMPLX_0:def 7
      .= t*(psi.(t"*x) + r) by A13,Def3;
    hence thesis by A20,A26,A27,A25,XREAL_1:64;
  end;
  suppose
A28: t < 0;
    -y29 in Lin{v} by A16,RLSUB_1:22;
    then -y29 in X + Lin{v} by RLSUB_2:2;
    then reconsider y2 = -y29 as VECTOR of X + Lin{v} by STRUCT_0:def 5;
    reconsider a = psi.((-t)"*x) - q.((-t)"*y1 - v) as R_eal by XBOOLE_0:def 3
,XXREAL_0:def 4;
A29: y = y1 - -y29 by A17,RLVECT_1:17;
A30: -y29 = (-t)*v by A18,RLVECT_4:3;
    then y2 = (-t)*x0 by RLSUB_1:14;
    then
A31: y = x - (-t)*x0 by A29,RLSUB_1:16;
A32: (-t)"*x1 = (-t)"*y1 by RLSUB_1:14;
    then (-t)"*x1 = (-t)"*x by RLSUB_1:14;
    then fi.((-t)"*x1) = psi.((-t)"*x) by A12,FUNCT_1:49;
    then psi.((-t)"*x) - q.((-t)"*y1 - v) in A by A32;
    then a <= sup A by XXREAL_2:4;
    then
A33: psi.((-t)"*x) <= r + q.((-t)"*y1 - v) by XREAL_1:20;
A34: -t > 0 by A28,XREAL_1:58;
    (-t)"*u = (-t)"*y1 - (-t)"*-y29 by A14,A29,RLVECT_1:34
      .= (-t)"*y1 - (-t)"*(-t)*v by A30,RLVECT_1:def 7
      .= (-t)"*y1 - 1*v by A34,XCMPLX_0:def 7
      .= (-t)"*y1 - v by RLVECT_1:def 8;
    then psi.((-t)"*x) - r <= q.((-t)"*u) by A33,XREAL_1:20;
    then
A35: psi.((-t)"*x) - r <= (-t)"*(q.u) by A34,Def4;
A36: (-t)*((-t)"*(q.u)) = (-t)*(-t)"*(q.u) .= 1*(q.u) by A34,XCMPLX_0:def 7
      .= q.u;
    psi.(x - (-t)*x0) = psi.x - psi.((-t)*x0) by Th19
      .= 1*(psi.x - (-t)*psi.x0) by Def3
      .= (-t)*(-t)"*(psi.x - (-t)*psi.x0) by A34,XCMPLX_0:def 7
      .= (-t)*((-t)"*(psi.x) - (-t)"*(-t)*psi.x0)
      .= (-t)*((-t)"*(psi.x) - 1*psi.x0) by A34,XCMPLX_0:def 7
      .= (-t)*(psi.((-t)"*x) - r) by A13,Def3;
    hence thesis by A28,A31,A36,A35,XREAL_1:64;
  end;
end;

Lm2: the RLSStruct of V is RealLinearSpace
proof
A1: for v9,w9 be VECTOR of V, v,w be VECTOR of the RLSStruct of V st v = v9
  & w = w9 holds v + w = v9 + w9 & for r be Real holds r *v = r* v9;
  the RLSStruct of V is Abelian add-associative right_zeroed
  right_complementable vector-distributive scalar-distributive
  scalar-associative scalar-unital
  proof
    hereby
      let v,w be VECTOR of the RLSStruct of V;
      reconsider v9 = v, w9 = w as VECTOR of V;
      thus v + w = w9 + v9 by A1
        .= w + v;
    end;
    hereby
      let u,v,w be VECTOR of the RLSStruct of V;
      reconsider u9 = u, v9 = v, w9 = w as VECTOR of V;
      thus (u + v) + w = (u9 + v9) + w9 .= u9 + (v9 + w9) by RLVECT_1:def 3
        .= u + (v + w);
    end;
    hereby
      let v be VECTOR of the RLSStruct of V;
      reconsider v9 = v as VECTOR of V;
      thus v + 0.the RLSStruct of V = v9 + 0.V .= v by RLVECT_1:4;
    end;
    thus the RLSStruct of V is right_complementable
    proof
      let v be VECTOR of the RLSStruct of V;
      reconsider v9 = v as VECTOR of V;
      consider w9 being VECTOR of V such that
A2:   v9 + w9 = 0.V by ALGSTR_0:def 11;
      reconsider w = w9 as VECTOR of the RLSStruct of V;
      take w;
      thus thesis by A2;
    end;
    hereby
      let a be real number, v,w be VECTOR of the RLSStruct of V;
      reconsider v9 = v, w9 = w as VECTOR of V;
      thus a * (v + w) = a * (v9 + w9) .= a * v9 + a * w9 by RLVECT_1:def 5
        .= a * v + a * w;
    end;
    hereby
      let a,b be real number, v be VECTOR of the RLSStruct of V;
      reconsider v9 = v as VECTOR of V;
      thus (a + b) * v = (a + b) * v9 .= a * v9 + b * v9 by RLVECT_1:def 6
        .= a * v + b * v;
    end;
    hereby
      let a,b be real number, v be VECTOR of the RLSStruct of V;
      reconsider v9 = v as VECTOR of V;
      thus (a * b) * v = (a * b) * v9 .= a * (b * v9) by RLVECT_1:def 7
        .= a * (b * v);
    end;
    let v be VECTOR of the RLSStruct of V;
    reconsider v9 = v as VECTOR of V;
    thus 1 * v = 1 * v9 .= v by RLVECT_1:def 8;
  end;
  hence thesis;
end;

Lm3: for V9,W9 being RealLinearSpace st V9 = the RLSStruct of V for W being
Subspace of V st W9 = the RLSStruct of W holds W9 is Subspace of V9
proof
  let V9,W9 be RealLinearSpace such that
A1: V9 = the RLSStruct of V;
  let W be Subspace of V;
  assume
A2: W9 = the RLSStruct of W;
  hence the carrier of W9 c= the carrier of V9 by A1,RLSUB_1:def 2;
  thus 0.W9 = 0.W by A2
    .= 0.V by RLSUB_1:def 2
    .= 0.V9 by A1;
  thus the addF of W9 = (the addF of V9)||the carrier of W9 by A1,A2,
RLSUB_1:def 2;
  thus the Mult of W9 = (the Mult of V9)|[:REAL, the carrier of W9:] by A1,A2,
RLSUB_1:def 2;
end;

Lm4: for V9 being RealLinearSpace st V9 = the RLSStruct of V for f being
linear-Functional of V9 holds f is linear-Functional of V
proof
  let V9 be RealLinearSpace such that
A1: V9 = the RLSStruct of V;
  let f be linear-Functional of V9;
  reconsider f9 = f as Functional of V by A1;
A2: f9 is homogeneous
  proof
    let x be VECTOR of V, r be Real;
    reconsider x9 = x as VECTOR of V9 by A1;
    thus f9.(r*x) = f9.(r*x9) by A1
      .= r*f9.x by Def3;
  end;
  f9 is additive
  proof
    let x,y be VECTOR of V;
    reconsider x9 = x, y9 = y as VECTOR of V9 by A1;
    thus f9.(x+y) = f.(x9+y9) by A1
      .= f9.x+f9.y by Def2;
  end;
  hence thesis by A2;
end;

Lm5: for V9 being RealLinearSpace st V9 = the RLSStruct of V for f being
linear-Functional of V holds f is linear-Functional of V9
proof
  let V9 be RealLinearSpace such that
A1: V9 = the RLSStruct of V;
  let f be linear-Functional of V;
  reconsider f9 = f as Functional of V9 by A1;
A2: f9 is homogeneous
  proof
    let x be VECTOR of V9, r be Real;
    reconsider x9 = x as VECTOR of V by A1;
    thus f9.(r*x) = f9.(r*x9) by A1
      .= r*f9.x by Def3;
  end;
  f9 is additive
  proof
    let x,y be VECTOR of V9;
    reconsider x9 = x, y9 = y as VECTOR of V by A1;
    thus f9.(x+y) = f.(x9+y9) by A1
      .= f9.x+f9.y by Def2;
  end;
  hence thesis by A2;
end;

theorem Th22:
  for V being RealLinearSpace, X being Subspace of V, q being
  Banach-Functional of V, fi being linear-Functional of X st for x being VECTOR
  of X, v being VECTOR of V st x=v holds fi.x <= q.v ex psi being
  linear-Functional of V st psi|the carrier of X=fi & for x being VECTOR of V
  holds psi.x <= q.x
proof
  let V be RealLinearSpace, X be Subspace of V, q be Banach-Functional of V,
  fi be linear-Functional of X;
  the carrier of X c= the carrier of V by RLSUB_1:def 2;
  then fi in PFuncs(the carrier of X,REAL) & PFuncs(the carrier of X,REAL) c=
  PFuncs(the carrier of V,REAL) by PARTFUN1:45,50;
  then reconsider fi9 = fi as Element of PFuncs(the carrier of V,REAL);
  reconsider RLS = the RLSStruct of V as RealLinearSpace by Lm2;
  defpred P[Element of PFuncs(the carrier of V,REAL)] means ex Y being
  Subspace of V st the carrier of X c= the carrier of Y & $1|the carrier of X =
fi & ex f9 being linear-Functional of Y st $1 = f9 & for y being VECTOR of Y, v
  being VECTOR of V st y = v holds f9.y <= q.v;
  reconsider A = { f where f is Element of PFuncs(the carrier of V,REAL): P[f]
  } as Subset of PFuncs(the carrier of V,REAL) from DOMAIN_1:sch 7;
A1: fi9|the carrier of X = fi by RELSET_1:19;
  assume
  for x being VECTOR of X, v being VECTOR of V st x=v holds fi.x <= q. v;
  then fi in A by A1;
  then reconsider A as non empty Subset of PFuncs(the carrier of V,REAL);
  defpred P[set, set] means $1 c= $2;
A2: for x,y being Element of A st P[x,y] & P[y,x] holds x = y by
XBOOLE_0:def 10;
A3: for x,y,z being Element of A st P[x,y] & P[y,z] holds P[x,z] by XBOOLE_1:1;
A4: now
    let B be set such that
A5: B c= A and
A6: for x,y being Element of A st x in B & y in B holds P[x,y] or P[y ,x];
    per cases;
    suppose
A7:   B = {};
      set u = the Element of A;
      take u;
      let x be Element of A;
      assume x in B;
      hence P[x,u] by A7;
    end;
    suppose
A8:   B <> {};
A9:   B is c=-linear
      proof
        let x,y be set;
        assume x in B & y in B;
        hence x c= y or y c= x by A5,A6;
      end;
      B is Subset of PFuncs(the carrier of V,REAL) by A5,XBOOLE_1:1;
      then reconsider
      u = union B as Element of PFuncs(the carrier of V,REAL) by A9,TREES_2:40;
      reconsider E = B as non empty functional set by A5,A8;
      set t = the Element of B;
      set K = { dom g where g is Element of E: not contradiction };
A10:  dom u = union K by FUNCT_1:110;
A11:  now
        let t be set;
        assume t in A;
        then consider
        f being Element of PFuncs(the carrier of V,REAL) such that
A12:    t = f and
A13:    ex Y being Subspace of V st the carrier of X c= the carrier
of Y & f|the carrier of X = fi & ex f9 being linear-Functional of Y st f = f9 &
for y being VECTOR of Y, v being VECTOR of V st y = v holds f9.y <= q.v;
        consider Y being Subspace of V such that
A14:    the carrier of X c= the carrier of Y and
A15:    f|the carrier of X = fi and
A16:    ex f9 being linear-Functional of Y st f = f9 & for y being
        VECTOR of Y, v being VECTOR of V st y = v holds f9.y <= q.v by A13;
        take Y;
        consider f9 being linear-Functional of Y such that
A17:    f = f9 and
A18:    for y being VECTOR of Y, v being VECTOR of V st y = v holds
        f9.y <= q.v by A16;
        reconsider f = f9 as linear-Functional of Y;
        take f;
        thus t = f by A12,A17;
        thus the carrier of X c= the carrier of Y by A14;
        thus f|the carrier of X = fi by A15,A17;
        thus for y being VECTOR of Y, v being VECTOR of V st y = v holds f.y
        <= q.v by A18;
      end;
A19:  now
        let x be set;
        assume x in { dom g where g is Element of E: not contradiction };
        then consider g being Element of E such that
A20:    dom g = x;
        g in A by A5,TARSKI:def 3;
        then consider
        Y being Subspace of V, f9 being linear-Functional of Y such
        that
A21:    g = f9 and
        the carrier of X c= the carrier of Y and
        f9|the carrier of X = fi and
        for y being VECTOR of Y, v being VECTOR of V st y = v holds f9.y
        <= q.v by A11;
        dom g = the carrier of Y by A21,FUNCT_2:def 1;
        hence x c= the carrier of V by A20,RLSUB_1:def 2;
      end;
      t in A by A5,A8,TARSKI:def 3;
      then ex Y being Subspace of V, f9 being linear-Functional of Y st t = f9
& the carrier of X c= the carrier of Y & f9|the carrier of X = fi & for y being
      VECTOR of Y, v being VECTOR of V st y = v holds f9.y <= q.v by A11;
      then u <> {} by A8,XBOOLE_1:3,ZFMISC_1:74;
      then reconsider D = dom u as non empty Subset of V by A10,A19,ZFMISC_1:76
;
      D is linearly-closed
      proof
        hereby
          let v,u be Element of V;
          assume that
A22:      v in D and
A23:      u in D;
          consider D1 being set such that
A24:      v in D1 and
A25:      D1 in K by A10,A22,TARSKI:def 4;
          consider g1 being Element of E such that
A26:      D1 = dom g1 by A25;
          consider D2 being set such that
A27:      u in D2 and
A28:      D2 in K by A10,A23,TARSKI:def 4;
          consider g2 being Element of E such that
A29:      D2 = dom g2 by A28;
          g1 in A & g2 in A by A5,TARSKI:def 3;
          then g1 c= g2 or g2 c= g1 by A6;
          then consider g being Element of E such that
A30:      g1 c= g and
A31:      g2 c= g;
          g in A by A5,TARSKI:def 3;
          then consider
          Y being Subspace of V, f9 being linear-Functional of Y such
          that
A32:      g = f9 and
          the carrier of X c= the carrier of Y and
          f9|the carrier of X = fi and
          for y being VECTOR of Y, v being VECTOR of V st y = v holds f9.y
          <= q.v by A11;
A33:      dom g = the carrier of Y by A32,FUNCT_2:def 1;
          D2 c= dom g by A29,A31,RELAT_1:11;
          then
A34:      u in Y by A27,A33,STRUCT_0:def 5;
          D1 c= dom g by A26,A30,RELAT_1:11;
          then v in Y by A24,A33,STRUCT_0:def 5;
          then v + u in Y by A34,RLSUB_1:20;
          then
A35:      v + u in dom g by A33,STRUCT_0:def 5;
          dom g in K;
          hence v + u in D by A10,A35,TARSKI:def 4;
        end;
        let a be Real, v be Element of V;
        assume v in D;
        then consider D1 being set such that
A36:    v in D1 and
A37:    D1 in K by A10,TARSKI:def 4;
        consider g being Element of E such that
A38:    D1 = dom g by A37;
        g in A by A5,TARSKI:def 3;
        then consider
        Y being Subspace of V, f9 being linear-Functional of Y such
        that
A39:    g = f9 and
        the carrier of X c= the carrier of Y and
        f9|the carrier of X = fi and
        for y being VECTOR of Y, v being VECTOR of V st y = v holds f9.y
        <= q.v by A11;
A40:    dom g = the carrier of Y by A39,FUNCT_2:def 1;
        then v in Y by A36,A38,STRUCT_0:def 5;
        then a * v in Y by RLSUB_1:21;
        then
A41:    a * v in dom g by A40,STRUCT_0:def 5;
        dom g in K;
        hence thesis by A10,A41,TARSKI:def 4;
      end;
      then consider Y being strict Subspace of V such that
A42:  the carrier of Y = dom u by RLSUB_1:35;
      set t = the Element of dom u;
      consider XX being set such that
      t in XX and
A43:  XX in K by A10,A42,TARSKI:def 4;
      ex f being Function st u = f & dom f c= the carrier of V & rng f c=
      REAL by PARTFUN1:def 3;
      then reconsider f9 = u as Function of the carrier of Y, REAL by A42,
FUNCT_2:def 1,RELSET_1:4;
      reconsider f9 as Functional of Y;
      consider gg being Element of E such that
A44:  XX = dom gg by A43;
A45:  f9 is additive
      proof
        let x,y be VECTOR of Y;
        consider XXx being set such that
A46:    x in XXx and
A47:    XXx in K by A10,A42,TARSKI:def 4;
        consider ggx being Element of E such that
A48:    XXx = dom ggx by A47;
        consider XXy being set such that
A49:    y in XXy and
A50:    XXy in K by A10,A42,TARSKI:def 4;
        consider ggy being Element of E such that
A51:    XXy = dom ggy by A50;
        ggx in A & ggy in A by A5,TARSKI:def 3;
        then ggx c= ggy or ggy c= ggx by A6;
        then consider gg being Element of E such that
A52:    gg = ggx or gg = ggy and
A53:    ggx c= gg & ggy c= gg;
        gg in A by A5,TARSKI:def 3;
        then consider
        YY being Subspace of V, ff being linear-Functional of YY such
        that
A54:    gg = ff and
        the carrier of X c= the carrier of YY and
        ff|the carrier of X = fi and
        for y being VECTOR of YY, v being VECTOR of V st y = v holds ff.y
        <= q.v by A11;
        dom ggx c= dom gg & dom ggy c= dom gg by A53,RELAT_1:11;
        then reconsider x9 = x, y9 = y as VECTOR of YY by A46,A48,A49,A51,A54,
FUNCT_2:def 1;
A55:    ff c= f9 by A54,ZFMISC_1:74;
A56:    dom ff = the carrier of YY by FUNCT_2:def 1;
        then YY is Subspace of Y by A10,A42,A47,A48,A50,A51,A52,A54,RLSUB_1:28
,ZFMISC_1:74;
        then x + y = x9 + y9 by RLSUB_1:13;
        hence f9.(x+y) = ff.(x9+y9) by A56,A55,GRFUNC_1:2
          .= ff.x9 + ff.y9 by Def2
          .= f9.x+ff.y9 by A56,A55,GRFUNC_1:2
          .= f9.x+f9.y by A56,A55,GRFUNC_1:2;
      end;
      f9 is homogeneous
      proof
        let x be VECTOR of Y, r be Real;
        consider XX being set such that
A57:    x in XX and
A58:    XX in K by A10,A42,TARSKI:def 4;
        consider gg being Element of E such that
A59:    XX = dom gg by A58;
        gg in A by A5,TARSKI:def 3;
        then consider
        YY being Subspace of V, ff being linear-Functional of YY such
        that
A60:    gg = ff and
        the carrier of X c= the carrier of YY and
        ff|the carrier of X = fi and
        for y being VECTOR of YY, v being VECTOR of V st y = v holds ff.y
        <= q.v by A11;
        reconsider x9 = x as VECTOR of YY by A57,A59,A60,FUNCT_2:def 1;
A61:    ff c= f9 by A60,ZFMISC_1:74;
A62:    dom ff = the carrier of YY by FUNCT_2:def 1;
        then YY is Subspace of Y by A10,A42,A58,A59,A60,RLSUB_1:28,ZFMISC_1:74;
        then r*x = r*x9 by RLSUB_1:14;
        hence f9.(r*x) = ff.(r*x9) by A62,A61,GRFUNC_1:2
          .= r*ff.x9 by Def3
          .= r*f9.x by A62,A61,GRFUNC_1:2;
      end;
      then reconsider f9 as linear-Functional of Y by A45;
A63:  now
        let y be VECTOR of Y, v be VECTOR of V such that
A64:    y = v;
        consider XX being set such that
A65:    y in XX and
A66:    XX in K by A10,A42,TARSKI:def 4;
        consider gg being Element of E such that
A67:    XX = dom gg by A66;
        gg in A by A5,TARSKI:def 3;
        then consider
        YY being Subspace of V, ff being linear-Functional of YY such
        that
A68:    gg = ff and
        the carrier of X c= the carrier of YY and
        ff|the carrier of X = fi and
A69:    for y being VECTOR of YY, v being VECTOR of V st y = v holds
        ff.y <= q.v by A11;
        reconsider y9 = y as VECTOR of YY by A65,A67,A68,FUNCT_2:def 1;
A70:    dom ff = the carrier of YY & ff c= f9 by A68,FUNCT_2:def 1,ZFMISC_1:74;
        ff.y9 <= q.v by A64,A69;
        hence f9.y <= q.v by A70,GRFUNC_1:2;
      end;
      gg in A by A5,TARSKI:def 3;
      then consider
      YY being Subspace of V, ff being linear-Functional of YY such
      that
A71:  gg = ff and
A72:  the carrier of X c= the carrier of YY and
A73:  ff|the carrier of X = fi and
      for y being VECTOR of YY, v being VECTOR of V st y = v holds ff.y <=
      q.v by A11;
      the carrier of X c= dom ff by A72,FUNCT_2:def 1;
      then
A74:  u|the carrier of X = fi by A71,A73,GRFUNC_1:27,ZFMISC_1:74;
A75:  XX c= dom u by A10,A43,ZFMISC_1:74;
      XX = the carrier of YY by A44,A71,FUNCT_2:def 1;
      then the carrier of X c= the carrier of Y by A42,A72,A75,XBOOLE_1:1;
      then u in A by A74,A63;
      then reconsider u as Element of A;
      take u;
      let x be Element of A;
      assume x in B;
      hence P[x,u] by ZFMISC_1:74;
    end;
  end;
A76: for x being Element of A holds P[x,x];
  consider psi being Element of A such that
A77: for chi being Element of A st psi <> chi holds not P[psi,chi] from
  ORDERS_1:sch 1(A76,A2,A3,A4);
  psi in A;
  then consider f being Element of PFuncs(the carrier of V,REAL) such that
A78: f = psi and
A79: ex Y being Subspace of V st the carrier of X c= the carrier of Y &
f|the carrier of X = fi & ex f9 being linear-Functional of Y st f = f9 & for y
  being VECTOR of Y, v being VECTOR of V st y = v holds f9.y <= q.v;
  consider Y being Subspace of V such that
A80: the carrier of X c= the carrier of Y and
A81: f|the carrier of X = fi and
A82: ex f9 being linear-Functional of Y st f = f9 & for y being VECTOR
  of Y, v being VECTOR of V st y = v holds f9.y <= q.v by A79;
  reconsider RLSY = the RLSStruct of Y as RealLinearSpace by Lm2;
  consider f9 being linear-Functional of Y such that
A83: f = f9 and
A84: for y being VECTOR of Y, v being VECTOR of V st y = v holds f9.y
  <= q.v by A82;
A85: RLSY is Subspace of RLS by Lm3;
A86: now
    assume the RLSStruct of Y <> the RLSStruct of V;
    then
A87: the carrier of Y <> the carrier of V by A85,RLSUB_1:32;
    the carrier of Y c= the carrier of V by RLSUB_1:def 2;
    then the carrier of Y c< the carrier of V by A87,XBOOLE_0:def 8;
    then consider v being set such that
A88: v in the carrier of V and
A89: not v in the carrier of Y by XBOOLE_0:6;
    reconsider v as VECTOR of V by A88;
    consider phi being linear-Functional of Y + Lin{v} such that
A90: phi|the carrier of Y = f9 and
A91: for x being VECTOR of Y + Lin{v}, v being VECTOR of V st x = v
    holds phi.x <= q.v by A84,A89,Lm1;
A92: rng phi c= REAL by RELAT_1:def 19;
    the carrier of Y c= the carrier of Y + Lin{v} by Th1;
    then
A93: the carrier of X c= the carrier of Y + Lin{v} by A80,XBOOLE_1:1;
A94: dom phi = the carrier of Y + Lin{v} by FUNCT_2:def 1;
    then dom phi c= the carrier of V by RLSUB_1:def 2;
    then reconsider phi as Element of PFuncs(the carrier of V,REAL) by A92,
PARTFUN1:def 3;
    (the carrier of Y) /\ the carrier of X = the carrier of X by A80,
XBOOLE_1:28;
    then phi|the carrier of X = fi by A81,A83,A90,RELAT_1:71;
    then
A95: phi in A by A91,A93;
    v in Lin{v} by RLVECT_4:9;
    then
A96: v in the carrier of Lin{v} by STRUCT_0:def 5;
    reconsider phi as Element of A by A95;
    the carrier of Lin{v} c= the carrier of Lin{v} + Y by Th1;
    then dom f9 = the carrier of Y & v in the carrier of Lin{v} + Y by A96,
FUNCT_2:def 1;
    then phi <> psi by A78,A83,A89,A94,RLSUB_2:5;
    hence contradiction by A77,A78,A83,A90,RELAT_1:59;
  end;
  reconsider ggh = f9 as linear-Functional of RLSY by Lm5;
  f = ggh by A83;
  then reconsider psi as linear-Functional of V by A78,A86,Lm4;
  take psi;
  thus psi|the carrier of X = fi by A78,A81;
  let x be VECTOR of V;
  thus thesis by A78,A82,A86;
end;

theorem Th23:
  for V being RealNormSpace holds the normF of V is
  absolutely_homogeneous subadditive Functional of V
proof
  let V be RealNormSpace;
  reconsider N = the normF of V as Functional of V;
A1: N is subadditive
  proof
    let x,y be VECTOR of V;
A2: N.(x+y) = ||.x+y.|| by NORMSP_0:def 1;
    N.(x) = ||.x.|| & N.(y) = ||.y.|| by NORMSP_0:def 1;
    hence thesis by A2,NORMSP_1:def 1;
  end;
  N is absolutely_homogeneous
  proof
    let x be VECTOR of V, r be Real;
    thus N.(r*x) = ||.r*x.|| by NORMSP_0:def 1
      .= abs(r)*||.x.|| by NORMSP_1:def 1
      .= abs(r)*N.x by NORMSP_0:def 1;
  end;
  hence thesis by A1;
end;

::$N Hahn-Banach Theorem (real spaces)
theorem
  for V being RealNormSpace, X being Subspace of V, fi being
  linear-Functional of X st for x being VECTOR of X, v being VECTOR of V st x=v
holds fi.x <= ||.v.|| ex psi being linear-Functional of V st psi|the carrier of
  X=fi & for x being VECTOR of V holds psi.x <= ||.x.||
proof
  let V be RealNormSpace, X be Subspace of V, fi be linear-Functional of X
  such that
A1: for x being VECTOR of X, v being VECTOR of V st x=v holds fi.x <= ||.v.||;
  reconsider q = the normF of V as Banach-Functional of V by Th23;
  now
    let x be VECTOR of X, v be VECTOR of V such that
A2: x=v;
    q.v = ||.v.|| by NORMSP_0:def 1;
    hence fi.x <= q.v by A1,A2;
  end;
  then consider psi being linear-Functional of V such that
A3: psi|the carrier of X=fi and
A4: for x being VECTOR of V holds psi.x <= q.x by Th22;
  take psi;
  thus psi|the carrier of X=fi by A3;
  let x be VECTOR of V;
  q.x = ||.x.|| by NORMSP_0:def 1;
  hence thesis by A4;
end;