rsspace.miz



    begin

    definition

      :: RSSPACE:def1

      func the_set_of_RealSequences -> non empty set equals ( Funcs ( NAT , REAL ));

      coherence ;

    end

    definition

      let a be object;

      :: RSSPACE:def2

      func seq_id (a) -> Real_Sequence equals

      : Def2: a;

      coherence by A1, FUNCT_2: 66;

    end

    definition

      ::$Canceled

      :: RSSPACE:def6

      func Zeroseq -> Element of the_set_of_RealSequences equals ( seq_const 0 );

      coherence by FUNCT_2: 8;

    end

    registration

      let x be Element of the_set_of_RealSequences ;

      reduce ( seq_id x) to x;

      reducibility by Def2;

    end

    registration

      let x be Real_Sequence;

      reduce ( seq_id x) to x;

      reducibility

      proof

        x in the_set_of_RealSequences by FUNCT_2: 8;

        hence thesis by Def2;

      end;

    end

    theorem :: RSSPACE:1

    for x be Real_Sequence holds ( seq_id x) = x;

    definition

      :: RSSPACE:def7

      func Linear_Space_of_RealSequences -> strict RLSStruct equals ( RealVectSpace NAT );

      coherence ;

    end

    registration

      let x be Element of Linear_Space_of_RealSequences ;

      reduce ( seq_id x) to x;

      reducibility by Def2;

    end

    registration

      cluster Linear_Space_of_RealSequences -> non empty;

      coherence ;

    end

    theorem :: RSSPACE:2

    for v,w be VECTOR of Linear_Space_of_RealSequences holds (v + w) = (( seq_id v) + ( seq_id w))

    proof

      let v,w be VECTOR of Linear_Space_of_RealSequences ;

      reconsider v1 = v, w1 = w as Element of ( Funcs ( NAT , REAL ));

      (( RealFuncAdd NAT ) . (v1,w1)) = (( seq_id v) + ( seq_id w))

      proof

        let n be Element of NAT ;

        

        thus ((( RealFuncAdd NAT ) . (v1,w1)) . n) = ((v1 . n) + (w1 . n)) by FUNCSDOM: 1

        .= ((( seq_id v) + ( seq_id w)) . n) by VALUED_1: 1;

      end;

      hence thesis;

    end;

    theorem :: RSSPACE:3

    

     Th3: for r be Real, v be VECTOR of Linear_Space_of_RealSequences holds (r * v) = (r (#) ( seq_id v))

    proof

      let r be Real;

      let v be VECTOR of Linear_Space_of_RealSequences ;

      reconsider r1 = r as Element of REAL by XREAL_0:def 1;

      reconsider v1 = v as Element of ( Funcs ( NAT , REAL ));

      reconsider h = (( RealFuncExtMult NAT ) . (r1,v1)) as Real_Sequence by FUNCT_2: 66;

      h = (r (#) ( seq_id v))

      proof

        let n be Element of NAT ;

        

        thus (h . n) = (r * (v1 . n)) by FUNCSDOM: 4

        .= ((r (#) ( seq_id v)) . n) by VALUED_1: 6;

      end;

      hence thesis;

    end;

    registration

      cluster Linear_Space_of_RealSequences -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence ;

    end

    definition

      let X be RealLinearSpace;

      let X1 be Subset of X;

      :: RSSPACE:def8

      func Add_ (X1,X) -> BinOp of X1 equals

      : Def5: (the addF of X || X1);

      correctness

      proof

        

         A2: ( dom the addF of X) = [:the carrier of X, the carrier of X:] by FUNCT_2:def 1;

        

         A3: for z be object st z in [:X1, X1:] holds ((the addF of X || X1) . z) in X1

        proof

          let z be object such that

           A4: z in [:X1, X1:];

          consider r,x be object such that

           A5: r in X1 & x in X1 and

           A6: z = [r, x] by A4, ZFMISC_1:def 2;

          reconsider y = x, r1 = r as VECTOR of X by A5;

           [r, x] in ( dom (the addF of X || X1)) by A2, A4, A6, RELAT_1: 62, ZFMISC_1: 96;

          then ((the addF of X || X1) . z) = (r1 + y) by A6, FUNCT_1: 47;

          hence thesis by A1, A5;

        end;

        ( dom (the addF of X || X1)) = [:X1, X1:] by A2, RELAT_1: 62, ZFMISC_1: 96;

        hence thesis by A3, FUNCT_2: 3;

      end;

    end

    definition

      let X be RealLinearSpace;

      let X1 be Subset of X;

      :: RSSPACE:def9

      func Mult_ (X1,X) -> Function of [: REAL , X1:], X1 equals

      : Def6: (the Mult of X | [: REAL , X1:]);

      correctness

      proof

        

         A2: [: REAL , X1:] c= [: REAL , the carrier of X:] & ( dom the Mult of X) = [: REAL , the carrier of X:] by FUNCT_2:def 1, ZFMISC_1: 95;

        

         A3: for z be object st z in [: REAL , X1:] holds ((the Mult of X | [: REAL , X1:]) . z) in X1

        proof

          let z be object such that

           A4: z in [: REAL , X1:];

          consider r,x be object such that

           A5: r in REAL and

           A6: x in X1 and

           A7: z = [r, x] by A4, ZFMISC_1:def 2;

          reconsider r as Real by A5;

          reconsider y = x as VECTOR of X by A6;

           [r, x] in ( dom (the Mult of X | [: REAL , X1:])) by A2, A4, A7, RELAT_1: 62;

          then ((the Mult of X | [: REAL , X1:]) . z) = (r * y) by A7, FUNCT_1: 47;

          hence thesis by A1, A6;

        end;

        ( dom (the Mult of X | [: REAL , X1:])) = [: REAL , X1:] by A2, RELAT_1: 62;

        hence thesis by A3, FUNCT_2: 3;

      end;

    end

    definition

      let X be RealLinearSpace, X1 be Subset of X;

      :: RSSPACE:def10

      func Zero_ (X1,X) -> Element of X1 equals

      : Def7: ( 0. X);

      correctness

      proof

        set v = the Element of X1;

        v in X1 by A1;

        then

        reconsider v as Element of X;

        (v - v) = ( 0. X) by RLVECT_1: 15;

        hence thesis by A1, RLSUB_1: 3;

      end;

    end

    theorem :: RSSPACE:4

    for n be object holds (( seq_id Zeroseq ) . n) = 0

    proof

      set f = ( seq_id Zeroseq );

      let n be object;

      per cases ;

        suppose

         A1: n in ( dom f);

        ( dom f) = NAT by FUNCT_2:def 1;

        hence thesis by A1, FUNCOP_1: 7;

      end;

        suppose not n in ( dom f);

        hence thesis by FUNCT_1:def 2;

      end;

    end;

    theorem :: RSSPACE:5

    for f be Element of the_set_of_RealSequences st for n be Nat holds (( seq_id f) . n) = 0 holds f = Zeroseq

    proof

      let f be Element of the_set_of_RealSequences ;

      set g = ( seq_id f);

      assume

       A1: for n be Nat holds (g . n) = 0 ;

      

       A2: ( dom g) = NAT by FUNCT_2:def 1;

      for z be object st z in ( dom g) holds (g . z) = 0 by A1;

      hence f = Zeroseq by A2, FUNCOP_1: 11;

    end;

    ::$Canceled

    theorem :: RSSPACE:11

    

     Th4: for V be RealLinearSpace, V1 be Subset of V st V1 is linearly-closed non empty holds RLSStruct (# V1, ( Zero_ (V1,V)), ( Add_ (V1,V)), ( Mult_ (V1,V)) #) is Subspace of V

    proof

      let V be RealLinearSpace;

      let V1 be Subset of V such that

       A1: V1 is linearly-closed non empty;

      

       A2: ( Mult_ (V1,V)) = (the Mult of V | [: REAL , V1:]) by A1, Def6;

      ( Zero_ (V1,V)) = ( 0. V) & ( Add_ (V1,V)) = (the addF of V || V1) by A1, Def5, Def7;

      hence thesis by A1, A2, RLSUB_1: 24;

    end;

    definition

      :: RSSPACE:def11

      func the_set_of_l2RealSequences -> Subset of Linear_Space_of_RealSequences means

      : Def8: for x be object holds x in it iff x in the_set_of_RealSequences & (( seq_id x) (#) ( seq_id x)) is summable;

      existence

      proof

        defpred P[ object] means (( seq_id $1) (#) ( seq_id $1)) is summable;

        consider IT be set such that

         A1: for x be object holds x in IT iff x in the_set_of_RealSequences & P[x] from XBOOLE_0:sch 1;

        for x be object st x in IT holds x in the_set_of_RealSequences by A1;

        then IT is Subset of the_set_of_RealSequences by TARSKI:def 3;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of Linear_Space_of_RealSequences ;

        assume that

         A2: for x be object holds x in X1 iff x in the_set_of_RealSequences & (( seq_id x) (#) ( seq_id x)) is summable and

         A3: for x be object holds x in X2 iff x in the_set_of_RealSequences & (( seq_id x) (#) ( seq_id x)) is summable;

        thus X1 c= X2

        proof

          let x be object;

          assume

           A4: x in X1;

          then (( seq_id x) (#) ( seq_id x)) is summable by A2;

          hence thesis by A3, A4;

        end;

        let x be object;

        assume

         A5: x in X2;

        then (( seq_id x) (#) ( seq_id x)) is summable by A3;

        hence thesis by A2, A5;

      end;

    end

    registration

      cluster the_set_of_l2RealSequences -> linearly-closed non empty;

      coherence

      proof

        set W = the_set_of_l2RealSequences ;

        hereby

          let v,u be VECTOR of Linear_Space_of_RealSequences such that

           A4: v in W and

           A5: u in W;

          (( seq_id (v + u)) (#) ( seq_id (v + u))) is summable

          proof

            set r = (( seq_id (v + u)) (#) ( seq_id (v + u)));

            set q = (( seq_id u) (#) ( seq_id u));

            set p = (( seq_id v) (#) ( seq_id v));

            

             A6: for n be Nat holds 0 <= (r . n)

            proof

              let n be Nat;

              (r . n) = ((( seq_id (v + u)) . n) * (( seq_id (v + u)) . n)) by SEQ_1: 8;

              hence thesis by XREAL_1: 63;

            end;

            

             A7: for n be Nat holds (r . n) <= (((2 (#) p) + (2 (#) q)) . n)

            proof

              set s = ( seq_id v), t = ( seq_id u);

              let n be Nat;

              reconsider sn = (s . n), tn = (t . n) as Real;

              

               A8: (((2 (#) p) + (2 (#) q)) . n) = (((2 (#) p) . n) + ((2 (#) q) . n)) by SEQ_1: 7

              .= ((2 * (p . n)) + ((2 (#) q) . n)) by SEQ_1: 9

              .= ((2 * (p . n)) + (2 * (q . n))) by SEQ_1: 9

              .= ((2 * ((s . n) * (s . n))) + (2 * (q . n))) by SEQ_1: 8

              .= ((2 * (sn ^2 )) + (2 * (tn ^2 ))) by SEQ_1: 8;

              

               A9: 0 <= ((sn - tn) ^2 ) by XREAL_1: 63;

              reconsider vu = (v + u) as Element of ( Funcs ( NAT , REAL ));

              n in NAT by ORDINAL1:def 12;

              then (vu . n) = ((s . n) + (t . n)) by FUNCSDOM: 1;

              

              then (r . n) = (((s . n) + (t . n)) ^2 ) by SEQ_1: 8

              .= (((sn ^2 ) + ((2 * sn) * tn)) + (tn ^2 ));

              then ( 0 + (r . n)) <= (((((2 (#) p) + (2 (#) q)) . n) - (r . n)) + (r . n)) by A8, A9, XREAL_1: 7;

              hence thesis;

            end;

            (( seq_id u) (#) ( seq_id u)) is summable by A5, Def8;

            then

             A10: (2 (#) q) is summable by SERIES_1: 10;

            (( seq_id v) (#) ( seq_id v)) is summable by A4, Def8;

            then (2 (#) p) is summable by SERIES_1: 10;

            then ((2 (#) p) + (2 (#) q)) is summable by A10, SERIES_1: 7;

            hence thesis by A6, A7, SERIES_1: 20;

          end;

          hence (v + u) in W by Def8;

        end;

        hereby

          let a be Real;

          let v be VECTOR of Linear_Space_of_RealSequences ;

          assume v in W;

          then

           A2: (( seq_id v) (#) ( seq_id v)) is summable by Def8;

          (a * v) = (a (#) ( seq_id v)) by Th3;

          

          then (( seq_id (a * v)) (#) ( seq_id (a * v))) = (a (#) ((a (#) ( seq_id v)) (#) ( seq_id v))) by SEQ_1: 19

          .= (a (#) (a (#) (( seq_id v) (#) ( seq_id v)))) by SEQ_1: 18

          .= ((a * a) (#) (( seq_id v) (#) ( seq_id v))) by SEQ_1: 23;

          then (( seq_id (a * v)) (#) ( seq_id (a * v))) is summable by A2, SERIES_1: 10;

          hence (a * v) in W by Def8;

        end;

        (( seq_id Zeroseq ) (#) ( seq_id Zeroseq )) is absolutely_summable

        proof

          reconsider rseq = (( seq_id Zeroseq ) (#) ( seq_id Zeroseq )) as Real_Sequence;

          now

            let n be Nat;

            

            thus (rseq . n) = ((( seq_id Zeroseq ) . n) * (( seq_id Zeroseq ) . n)) by SEQ_1: 8

            .= ((( seq_id Zeroseq ) . n) * 0 ) by FUNCOP_1: 7, ORDINAL1:def 12

            .= 0 ;

          end;

          hence thesis by COMSEQ_3: 3;

        end;

        hence thesis by Def8;

      end;

    end

    theorem :: RSSPACE:12

     RLSStruct (# the_set_of_l2RealSequences , ( Zero_ ( the_set_of_l2RealSequences , Linear_Space_of_RealSequences )), ( Add_ ( the_set_of_l2RealSequences , Linear_Space_of_RealSequences )), ( Mult_ ( the_set_of_l2RealSequences , Linear_Space_of_RealSequences )) #) is Subspace of Linear_Space_of_RealSequences by Th4;

    theorem :: RSSPACE:13

    

     Th6: RLSStruct (# the_set_of_l2RealSequences , ( Zero_ ( the_set_of_l2RealSequences , Linear_Space_of_RealSequences )), ( Add_ ( the_set_of_l2RealSequences , Linear_Space_of_RealSequences )), ( Mult_ ( the_set_of_l2RealSequences , Linear_Space_of_RealSequences )) #) is RealLinearSpace by Th4;

    ::$Canceled

    definition

      :: RSSPACE:def12

      func l_scalar -> Function of [: the_set_of_l2RealSequences , the_set_of_l2RealSequences :], REAL means for x,y be object st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds (it . (x,y)) = ( Sum (( seq_id x) (#) ( seq_id y)));

      existence

      proof

        deffunc F( object, object) = ( Sum (( seq_id $1) (#) ( seq_id $2)));

        set X = the_set_of_l2RealSequences ;

        

         A1: for x,y be object st x in X & y in X holds F(x,y) in REAL by XREAL_0:def 1;

        ex f be Function of [:X, X:], REAL st for x,y be object st x in X & y in X holds (f . (x,y)) = F(x,y) from BINOP_1:sch 2( A1);

        hence thesis;

      end;

      uniqueness

      proof

        set X = the_set_of_l2RealSequences ;

        let scalar1,scalar2 be Function of [:X, X:], REAL such that

         A2: for x,y be object st x in X & y in X holds (scalar1 . (x,y)) = ( Sum (( seq_id x) (#) ( seq_id y))) and

         A3: for x,y be object st x in X & y in X holds (scalar2 . (x,y)) = ( Sum (( seq_id x) (#) ( seq_id y)));

        for x,y be set st x in X & y in X holds (scalar1 . (x,y)) = (scalar2 . (x,y))

        proof

          let x,y be set such that

           A4: x in X & y in X;

          

          thus (scalar1 . (x,y)) = ( Sum (( seq_id x) (#) ( seq_id y))) by A2, A4

          .= (scalar2 . (x,y)) by A3, A4;

        end;

        hence thesis;

      end;

    end

    definition

      :: RSSPACE:def13

      func l2_Space -> non empty UNITSTR equals UNITSTR (# the_set_of_l2RealSequences , ( Zero_ ( the_set_of_l2RealSequences , Linear_Space_of_RealSequences )), ( Add_ ( the_set_of_l2RealSequences , Linear_Space_of_RealSequences )), ( Mult_ ( the_set_of_l2RealSequences , Linear_Space_of_RealSequences )), l_scalar #);

      coherence ;

    end

    registration

      let x be Element of l2_Space ;

      reduce ( seq_id x) to x;

      reducibility

      proof

        x in the_set_of_RealSequences by Def8;

        hence thesis by Def2;

      end;

    end

    theorem :: RSSPACE:15

    

     Th7: for l be RLSStruct st the RLSStruct of l is RealLinearSpace holds l is RealLinearSpace

    proof

      let l be RLSStruct such that

       A1: the RLSStruct of l is RealLinearSpace;

      reconsider l as non empty RLSStruct by A1;

      reconsider l0 = RLSStruct (# the carrier of l, ( 0. l), the addF of l, the Mult of l #) as RealLinearSpace by A1;

      

       A2: l is Abelian

      proof

        let v,w be VECTOR of l;

        reconsider v1 = v as VECTOR of l0;

        reconsider w1 = w as VECTOR of l0;

        

        thus (v + w) = (v1 + w1)

        .= (w1 + v1)

        .= (w + v);

      end;

      

       A3: l is right_zeroed

      proof

        let v be VECTOR of l;

        reconsider v1 = v as VECTOR of l0;

        

        thus (v + ( 0. l)) = (v1 + ( 0. l0))

        .= v;

      end;

      

       A4: l is right_complementable

      proof

        let v be VECTOR of l;

        reconsider v1 = v as VECTOR of l0;

        consider w1 be VECTOR of l0 such that

         A5: (v1 + w1) = ( 0. l0) by ALGSTR_0:def 11;

        reconsider w = w1 as VECTOR of l;

        take w;

        thus thesis by A5;

      end;

      

       A6: for v be VECTOR of l holds (1 * v) = v

      proof

        let v be VECTOR of l;

        reconsider v1 = v as VECTOR of l0;

        

        thus (1 * v) = (1 * v1)

        .= v by RLVECT_1:def 8;

      end;

      

       A7: for a,b be Real holds for v be VECTOR of l holds ((a * b) * v) = (a * (b * v))

      proof

        let a,b be Real;

        let v be VECTOR of l;

        reconsider v1 = v as VECTOR of l0;

        

        thus ((a * b) * v) = ((a * b) * v1)

        .= (a * (b * v1)) by RLVECT_1:def 7

        .= (a * (b * v));

      end;

      

       A8: for a,b be Real holds for v be VECTOR of l holds ((a + b) * v) = ((a * v) + (b * v))

      proof

        let a,b be Real;

        let v be VECTOR of l;

        reconsider v1 = v as VECTOR of l0;

        

        thus ((a + b) * v) = ((a + b) * v1)

        .= ((a * v1) + (b * v1)) by RLVECT_1:def 6

        .= ((a * v) + (b * v));

      end;

      

       A9: for a be Real holds for v,w be VECTOR of l holds (a * (v + w)) = ((a * v) + (a * w))

      proof

        let a be Real;

        let v,w be VECTOR of l;

        reconsider v1 = v, w1 = w as VECTOR of l0;

        

        thus (a * (v + w)) = (a * (v1 + w1))

        .= ((a * v1) + (a * w1)) by RLVECT_1:def 5

        .= ((a * v) + (a * w));

      end;

      l is add-associative

      proof

        let u,v,w be VECTOR of l;

        reconsider u1 = u, v1 = v, w1 = w as VECTOR of l0;

        

        thus ((u + v) + w) = ((u1 + v1) + w1)

        .= (u1 + (v1 + w1)) by RLVECT_1:def 3

        .= (u + (v + w));

      end;

      hence thesis by A2, A3, A4, A9, A8, A7, A6, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;

    end;

    theorem :: RSSPACE:16

    for rseq be Real_Sequence st (for n be Nat holds (rseq . n) = 0 ) holds rseq is summable & ( Sum rseq) = 0

    proof

      let rseq be Real_Sequence such that

       A1: for n be Nat holds (rseq . n) = 0 ;

      

       A2: for m be Nat holds (( Partial_Sums rseq) . m) = 0

      proof

        defpred P[ Nat] means (rseq . $1) = (( Partial_Sums rseq) . $1);

        let m be Nat;

        

         A3: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat such that

           A4: (rseq . k) = (( Partial_Sums rseq) . k);

          

          thus (rseq . (k + 1)) = ( 0 + (rseq . (k + 1)))

          .= ((rseq . k) + (rseq . (k + 1))) by A1

          .= (( Partial_Sums rseq) . (k + 1)) by A4, SERIES_1:def 1;

        end;

        

         A5: P[ 0 ] by SERIES_1:def 1;

        for n be Nat holds P[n] from NAT_1:sch 2( A5, A3);

        

        hence (( Partial_Sums rseq) . m) = (rseq . m)

        .= 0 by A1;

      end;

      

       A6: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((( Partial_Sums rseq) . m) - 0 ).| < p

      proof

        let p be Real such that

         A7: 0 < p;

        take 0 ;

        let m be Nat such that 0 <= m;

         |.((( Partial_Sums rseq) . m) - 0 ).| = |.( 0 - 0 ).| by A2

        .= 0 by ABSVALUE:def 1;

        hence thesis by A7;

      end;

      then

       A8: ( Partial_Sums rseq) is convergent by SEQ_2:def 6;

      then ( lim ( Partial_Sums rseq)) = 0 by A6, SEQ_2:def 7;

      hence thesis by A8, SERIES_1:def 2, SERIES_1:def 3;

    end;

    theorem :: RSSPACE:17

    for rseq be Real_Sequence st (for n be Nat holds 0 <= (rseq . n)) & rseq is summable & ( Sum rseq) = 0 holds for n be Nat holds (rseq . n) = 0

    proof

      let rseq be Real_Sequence such that

       A1: for n be Nat holds 0 <= (rseq . n) and

       A2: rseq is summable and

       A3: ( Sum rseq) = 0 ;

      

       A4: ( Partial_Sums rseq) is bounded_above by A1, A2, SERIES_1: 17;

      

       A5: for n be Nat holds (( Partial_Sums rseq) . n) <= ( Sum rseq)

      proof

        let n be Nat;

        (( Partial_Sums rseq) . n) <= ( lim ( Partial_Sums rseq)) by A1, A4, SEQ_4: 37, SERIES_1: 16;

        hence thesis by SERIES_1:def 3;

      end;

      

       A6: ( Partial_Sums rseq) is non-decreasing by A1, SERIES_1: 16;

      now

        given n1 be Nat such that

         A7: (rseq . n1) <> 0 ;

        

         A8: for n be Nat holds 0 <= (( Partial_Sums rseq) . n)

        proof

          let n be Nat;

          

           A9: n = (n + 0 ) & (( Partial_Sums rseq) . 0 ) = (rseq . 0 ) by SERIES_1:def 1;

           0 <= (rseq . 0 ) by A1;

          hence thesis by A6, A9, SEQM_3: 5;

        end;

        (( Partial_Sums rseq) . n1) > 0

        proof

          now

            per cases ;

              case

               A10: n1 = 0 ;

              then (( Partial_Sums rseq) . n1) = (rseq . 0 ) by SERIES_1:def 1;

              hence thesis by A1, A7, A10;

            end;

              case

               A11: n1 <> 0 ;

              set nn = (n1 - 1);

              

               A12: (nn + 1) = n1 & 0 <= (rseq . n1) by A1;

              

               A13: n1 in NAT by ORDINAL1:def 12;

               0 <= n1 by NAT_1: 2;

              then ( 0 + 1) <= n1 by A11, INT_1: 7, A13;

              then

               A14: nn in NAT by INT_1: 5, A13;

              then

               A15: (( Partial_Sums rseq) . (nn + 1)) = ((( Partial_Sums rseq) . nn) + (rseq . (nn + 1))) by SERIES_1:def 1;

               0 <= (( Partial_Sums rseq) . nn) by A8, A14;

              hence thesis by A7, A12, A15;

            end;

          end;

          hence thesis;

        end;

        hence contradiction by A3, A5;

      end;

      hence thesis;

    end;

    registration

      cluster l2_Space -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence by Th6, Th7;

    end