hahnban.miz



    begin

    reserve V for RealLinearSpace;

    theorem :: HAHNBAN:1

    

     Th1: for W1,W2 be 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 object;

      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;

      x in W1 by A1;

      then x in { (v + u) where u,v be VECTOR of V : v in W1 & u in W2 } by A2;

      hence thesis by RLSUB_2:def 1;

    end;

    theorem :: HAHNBAN:2

    

     Th2: for W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds for v,v1,v2 be 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;

      hence thesis by A1, RLSUB_2:def 6;

    end;

    theorem :: HAHNBAN:3

    

     Th3: for W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds for v,v1,v2 be 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;

      hence thesis by A1, RLSUB_2:def 6;

    end;

    theorem :: HAHNBAN:4

    

     Th4: for W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds for v,v1,v2 be 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;

      hence thesis by A1, RLSUB_2:def 6;

    end;

    theorem :: HAHNBAN:5

    

     Th5: for W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds for v,v1,v2 be 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;

      then

       A4: v1 in W1 by A1, RLSUB_2:def 6;

      

       A5: ((v |-- (W1,W2)) `2 ) = v2 by A2;

      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 :: HAHNBAN:6

    

     Th6: for W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds for v be 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;

      hence thesis by A1, A2, Th2;

    end;

    theorem :: HAHNBAN:7

    

     Th7: for W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds for v be 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 :: HAHNBAN:8

    

     Th8: for V1 be Subspace of V, W1 be Subspace of V1, v be 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;

      hence thesis;

    end;

    theorem :: HAHNBAN:9

    

     Th9: for V1,V2,W be Subspace of V, W1,W2 be 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 be 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 be 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;

        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 :: HAHNBAN:10

    

     Th10: for W be Subspace of V holds for v be VECTOR of V, w be 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 be 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 be 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 :: HAHNBAN:11

    

     Th11: for v be VECTOR of V, X be Subspace of V st not v in X holds for y be VECTOR of (X + ( Lin {v})), W be 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 be 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 be 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 :: HAHNBAN:12

    

     Th12: for v be VECTOR of V, X be Subspace of V, y be VECTOR of (X + ( Lin {v})), W be 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 :: HAHNBAN:13

    

     Th13: for v be VECTOR of V, X be Subspace of V, y be VECTOR of (X + ( Lin {v})), W be Subspace of (X + ( Lin {v})) st v = y & X = W & not v in X holds for w be 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 :: HAHNBAN:14

    

     Th14: for v be VECTOR of V, W1,W2 be Subspace of V holds ex v1,v2 be 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 :: HAHNBAN:15

    

     Th15: for v be VECTOR of V, X be Subspace of V, y be VECTOR of (X + ( Lin {v})), W be Subspace of (X + ( Lin {v})) st v = y & X = W & not v in X holds for w be VECTOR of (X + ( Lin {v})) holds ex x be VECTOR of X, r be 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 be 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;

      v2 in ( Lin {y}) by A5, A4, Th4;

      then

      consider r be 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 :: HAHNBAN:16

    

     Th16: for v be VECTOR of V, X be Subspace of V, y be VECTOR of (X + ( Lin {v})), W be Subspace of (X + ( Lin {v})) st v = y & X = W & not v in X holds for w1,w2 be VECTOR of (X + ( Lin {v})), x1,x2 be VECTOR of X, r1,r2 be 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 :: HAHNBAN:17

    

     Th17: for v be VECTOR of V, X be Subspace of V, y be VECTOR of (X + ( Lin {v})), W be Subspace of (X + ( Lin {v})) st v = y & X = W & not v in X holds for w be VECTOR of (X + ( Lin {v})), x be VECTOR of X, t,r be 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;

      hence thesis by A4, A9, A8, A7, A6, Th2;

    end;

    begin

    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;

      :: HAHNBAN:def1

      attr IT is subadditive means

      : Def1: for x,y be VECTOR of V holds (IT . (x + y)) <= ((IT . x) + (IT . y));

      :: HAHNBAN:def2

      attr IT is additive means

      : Def2: for x,y be VECTOR of V holds (IT . (x + y)) = ((IT . x) + (IT . y));

      :: HAHNBAN:def3

      attr IT is homogeneous means

      : Def3: for x be VECTOR of V, r be Real holds (IT . (r * x)) = (r * (IT . x));

      :: HAHNBAN:def4

      attr IT is positively_homogeneous means

      : Def4: for x be VECTOR of V, r be Real st r > 0 holds (IT . (r * x)) = (r * (IT . x));

      :: HAHNBAN:def5

      attr IT is semi-homogeneous means for x be VECTOR of V, r be Real st r >= 0 holds (IT . (r * x)) = (r * (IT . x));

      :: HAHNBAN:def6

      attr IT is absolutely_homogeneous means for x be VECTOR of V, r be Real holds (IT . (r * x)) = ( |.r.| * (IT . x));

      :: HAHNBAN:def7

      attr IT is 0-preserving means (IT . ( 0. V)) = 0 ;

    end

    registration

      let V;

      cluster additive -> subadditive for Functional of V;

      coherence ;

      cluster homogeneous -> positively_homogeneous for Functional of V;

      coherence ;

      cluster semi-homogeneous -> positively_homogeneous for Functional of V;

      coherence ;

      cluster semi-homogeneous -> 0-preserving for Functional of V;

      coherence

      proof

        let f be Functional of V;

        assume

         A1: f is semi-homogeneous;

        

        thus (f . ( 0. V)) = (f . ( 0 * ( 0. V)))

        .= ( 0 * (f . ( 0. V))) by A1

        .= 0 ;

      end;

      cluster absolutely_homogeneous -> semi-homogeneous for Functional of V;

      coherence

      proof

        let f be Functional of V;

        assume

         A2: f is absolutely_homogeneous;

        let x be VECTOR of V, r be Real;

        assume r >= 0 ;

        then |.r.| = r by ABSVALUE:def 1;

        hence thesis by A2;

      end;

      cluster 0-preserving positively_homogeneous -> semi-homogeneous for Functional of V;

      coherence

      proof

        let f be Functional of V such that

         A3: f is 0-preserving and

         A4: f is positively_homogeneous;

        let x be VECTOR of V, r be Real such that

         A5: r >= 0 ;

        per cases by A5;

          suppose

           A6: r = 0 ;

          

          hence (f . (r * x)) = (f . ( 0. V)) by RLVECT_1: 10

          .= (r * (f . x)) by A3, A6;

        end;

          suppose r > 0 ;

          hence thesis by A4;

        end;

      end;

    end

    registration

      let V;

      cluster additive absolutely_homogeneous homogeneous for Functional of V;

      existence

      proof

        reconsider f = (the carrier of V --> ( In ( 0 , REAL ))) 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)) = ( |.r.| * 0 ) by FUNCOP_1: 7

          .= ( |.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 :: HAHNBAN:18

    

     Th18: for L be homogeneous Functional of V, v be 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 :: HAHNBAN:19

    

     Th19: for L be linear-Functional of V, v1,v2 be 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 :: HAHNBAN:20

    

     Th20: for L be 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)))

      .= ((L . ( 0. V)) + (L . ( 0. V))) by Def2;

      hence thesis;

    end;

    theorem :: HAHNBAN:21

    

     Th21: for X be Subspace of V, fi be linear-Functional of X, v be VECTOR of V, y be VECTOR of (X + ( Lin {v})) st v = y & not v in X holds for r be Real holds ex psi be 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 be VECTOR of X, s be 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 be VECTOR of X, s be Real such that

         A4: (e |-- (W1,( Lin {y}))) = [x, (s * v)] by A1, A2, Th15;

        reconsider u = ((fi . x) + (s * r)) as Element of REAL by XREAL_0:def 1;

        take u;

        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, RLVECT_1: 37;

          hence thesis by A4, A5;

        end;

      end;

      consider f be Function of the carrier of (X + ( Lin {v})), REAL such that

       A7: for e be VECTOR of (X + ( Lin {v})) holds P[e, (f . e)] from FUNCT_2:sch 3( A3);

       A8:

      now

        let a be object;

        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}));

        v1 in X;

        

        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);

        

        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);

      

       A12: f is additive

      proof

        let v1,v2 be VECTOR of (X + ( Lin {v}));

        consider x1 be VECTOR of X, s1 be 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;

        consider x2 be VECTOR of X, s2 be 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;

        ((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);

        

        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 be VECTOR of X, s0 be 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;

        ((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);

        

        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

      .= (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

    

     Lm1: for X be Subspace of V, v be VECTOR of V st not v in the carrier of X holds for q be Banach-Functional of V, fi be linear-Functional of X st for x be VECTOR of X, v be VECTOR of V st x = v holds (fi . x) <= (q . v) holds ex psi be linear-Functional of (X + ( Lin {v})) st (psi | the carrier of X) = fi & for x be VECTOR of (X + ( Lin {v})), v be 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;

      v in ( Lin {v}) by RLVECT_4: 9;

      then

       A2: v in the carrier of ( Lin {v});

      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 be VECTOR of X, v be VECTOR of V st x = v holds (fi . x) <= (q . v);

      set A = { ((fi . x) - (q . (y - v))) where x be VECTOR of X, y be VECTOR of V : x = y }, B = { ((fi . x) + (q . (v - y))) where x be VECTOR of X, y be 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))

        .= ((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 ExtReal;

        assume a in A;

        then

         A7: ex x1 be VECTOR of X, y1 be VECTOR of V st a = ((fi . x1) - (q . (y1 - v))) & x1 = y1;

        assume b in B;

        then ex x2 be VECTOR of X, y2 be 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 object;

        assume a in A;

        then ex x be VECTOR of X, y be VECTOR of V st a = ((fi . x) - (q . (y - v))) & x = y;

        hence thesis;

      end;

      

       A9: B c= REAL

      proof

        let b be object;

        assume b in B;

        then ex x be VECTOR of X, y be 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 by A9;

        take b;

        let x be ExtReal;

        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 Element of REAL by A11, XXREAL_2: 57;

      consider psi be 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}));

      then

      consider y1,y29 be 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}));

      reconsider x1 = x as VECTOR of X by A15;

      consider t be 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;

        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));

        

         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}));

        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}));

        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;

        

         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

      ( (Omega). V) is RealLinearSpace;

      hence thesis;

    end;

    

     Lm3: for V9,W9 be RealLinearSpace st V9 = the RLSStruct of V holds for W be 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 be RealLinearSpace st V9 = the RLSStruct of V holds for f be 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 be RealLinearSpace st V9 = the RLSStruct of V holds for f be 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 :: HAHNBAN:22

    

     Th22: for V be RealLinearSpace, X be Subspace of V, q be Banach-Functional of V, fi be linear-Functional of X st for x be VECTOR of X, v be VECTOR of V st x = v holds (fi . x) <= (q . v) holds ex psi be linear-Functional of V st (psi | the carrier of X) = fi & for x be 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, PARTFUN1: 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 be Subspace of V st the carrier of X c= the carrier of Y & ($1 | the carrier of X) = fi & ex f9 be linear-Functional of Y st $1 = f9 & for y be VECTOR of Y, v be VECTOR of V st y = v holds (f9 . y) <= (q . v);

      reconsider A = { f where f be 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;

      assume for x be VECTOR of X, v be 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 be Element of A st P[x, y] & P[y, x] holds x = y;

      

       A3: for x,y,z be 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 be 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 = the set of all ( dom g) where g be Element of E;

          

           A10: ( dom u) = ( union K) by FUNCT_1: 110;

           A11:

          now

            let t be set;

            assume t in A;

            then

            consider f be Element of ( PFuncs (the carrier of V, REAL )) such that

             A12: t = f and

             A13: ex Y be Subspace of V st the carrier of X c= the carrier of Y & (f | the carrier of X) = fi & ex f9 be linear-Functional of Y st f = f9 & for y be VECTOR of Y, v be VECTOR of V st y = v holds (f9 . y) <= (q . v);

            consider Y be 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 be linear-Functional of Y st f = f9 & for y be VECTOR of Y, v be VECTOR of V st y = v holds (f9 . y) <= (q . v) by A13;

            take Y;

            consider f9 be linear-Functional of Y such that

             A17: f = f9 and

             A18: for y be VECTOR of Y, v be 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 be VECTOR of Y, v be VECTOR of V st y = v holds (f . y) <= (q . v) by A18;

          end;

           A19:

          now

            let x be set;

            assume x in the set of all ( dom g) where g be Element of E;

            then

            consider g be Element of E such that

             A20: ( dom g) = x;

            g in A by A5;

            then

            consider Y be Subspace of V, f9 be 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 be VECTOR of Y, v be 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;

          then ex Y be Subspace of V, f9 be linear-Functional of Y st t = f9 & the carrier of X c= the carrier of Y & (f9 | the carrier of X) = fi & for y be VECTOR of Y, v be 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 be set such that

               A24: v in D1 and

               A25: D1 in K by A10, A22, TARSKI:def 4;

              consider g1 be Element of E such that

               A26: D1 = ( dom g1) by A25;

              consider D2 be set such that

               A27: u in D2 and

               A28: D2 in K by A10, A23, TARSKI:def 4;

              consider g2 be Element of E such that

               A29: D2 = ( dom g2) by A28;

              g1 in A & g2 in A by A5;

              then g1 c= g2 or g2 c= g1 by A6;

              then

              consider g be Element of E such that

               A30: g1 c= g and

               A31: g2 c= g;

              g in A by A5;

              then

              consider Y be Subspace of V, f9 be 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 be VECTOR of Y, v be 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;

              D1 c= ( dom g) by A26, A30, RELAT_1: 11;

              then v in Y by A24, A33;

              then (v + u) in Y by A34, RLSUB_1: 20;

              then

               A35: (v + u) in ( dom g) by A33;

              ( 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 be set such that

             A36: v in D1 and

             A37: D1 in K by A10, TARSKI:def 4;

            consider g be Element of E such that

             A38: D1 = ( dom g) by A37;

            g in A by A5;

            then

            consider Y be Subspace of V, f9 be 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 be VECTOR of Y, v be 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;

            then (a * v) in Y by RLSUB_1: 21;

            then

             A41: (a * v) in ( dom g) by A40;

            ( dom g) in K;

            hence thesis by A10, A41, TARSKI:def 4;

          end;

          then

          consider Y be 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 be set such that t in XX and

           A43: XX in K by A10, A42, TARSKI:def 4;

          ex f be 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 be 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 be set such that

             A46: x in XXx and

             A47: XXx in K by A10, A42, TARSKI:def 4;

            consider ggx be Element of E such that

             A48: XXx = ( dom ggx) by A47;

            consider XXy be set such that

             A49: y in XXy and

             A50: XXy in K by A10, A42, TARSKI:def 4;

            consider ggy be Element of E such that

             A51: XXy = ( dom ggy) by A50;

            ggx in A & ggy in A by A5;

            then ggx c= ggy or ggy c= ggx by A6;

            then

            consider gg be Element of E such that

             A52: gg = ggx or gg = ggy and

             A53: ggx c= gg & ggy c= gg;

            gg in A by A5;

            then

            consider YY be Subspace of V, ff be 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 be VECTOR of YY, v be 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 be set such that

             A57: x in XX and

             A58: XX in K by A10, A42, TARSKI:def 4;

            consider gg be Element of E such that

             A59: XX = ( dom gg) by A58;

            gg in A by A5;

            then

            consider YY be Subspace of V, ff be 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 be VECTOR of YY, v be 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 be set such that

             A65: y in XX and

             A66: XX in K by A10, A42, TARSKI:def 4;

            consider gg be Element of E such that

             A67: XX = ( dom gg) by A66;

            gg in A by A5;

            then

            consider YY be Subspace of V, ff be 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 be VECTOR of YY, v be 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;

          then

          consider YY be Subspace of V, ff be 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 be VECTOR of YY, v be 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;

          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 be Element of A holds P[x, x];

      consider psi be Element of A such that

       A77: for chi be 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 be Element of ( PFuncs (the carrier of V, REAL )) such that

       A78: f = psi and

       A79: ex Y be Subspace of V st the carrier of X c= the carrier of Y & (f | the carrier of X) = fi & ex f9 be linear-Functional of Y st f = f9 & for y be VECTOR of Y, v be VECTOR of V st y = v holds (f9 . y) <= (q . v);

      consider Y be 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 be linear-Functional of Y st f = f9 & for y be VECTOR of Y, v be 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 be linear-Functional of Y such that

       A83: f = f9 and

       A84: for y be VECTOR of Y, v be 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;

        then

        consider v be object 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 be linear-Functional of (Y + ( Lin {v})) such that

         A90: (phi | the carrier of Y) = f9 and

         A91: for x be VECTOR of (Y + ( Lin {v})), v be 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;

        

         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});

        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 :: HAHNBAN:23

    

     Th23: for V be 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

        .= ( |.r.| * ||.x.||) by NORMSP_1:def 1

        .= ( |.r.| * (N . x)) by NORMSP_0:def 1;

      end;

      hence thesis by A1;

    end;

    ::$Notion-Name

    theorem :: HAHNBAN:24

    for V be RealNormSpace, X be Subspace of V, fi be linear-Functional of X st for x be VECTOR of X, v be VECTOR of V st x = v holds (fi . x) <= ||.v.|| holds ex psi be linear-Functional of V st (psi | the carrier of X) = fi & for x be 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 be VECTOR of X, v be 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 be linear-Functional of V such that

       A3: (psi | the carrier of X) = fi and

       A4: for x be 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;