nbvectsp.miz



    begin

    reserve m,n,s for non zero Element of NAT ;

    

     Lm1: for n be non zero Nat, D be non empty set, p be Element of (n -tuples_on D) holds ( len p) = n & p is Element of (D * )

    proof

      let n be non zero Nat, D be non empty set, p be Element of (n -tuples_on D);

      p in (n -tuples_on D);

      then ex s be Element of (D * ) st p = s & ( len s) = n;

      hence thesis;

    end;

    theorem :: NBVECTSP:1

    

     Th1: for u1,v1,w1 be Element of (n -tuples_on BOOLEAN ) holds ( Op-XOR (( Op-XOR (u1,v1)),w1)) = ( Op-XOR (u1,( Op-XOR (v1,w1))))

    proof

      let u1,v1,w1 be Element of (n -tuples_on BOOLEAN );

      

       A1: ( len ( Op-XOR (( Op-XOR (u1,v1)),w1))) = n by Lm1;

      

       A2: ( len ( Op-XOR (u1,( Op-XOR (v1,w1))))) = n by Lm1;

      now

        let i be Nat;

        assume 1 <= i & i <= ( len ( Op-XOR (( Op-XOR (u1,v1)),w1)));

        then

         A3: i in ( Seg n) by A1;

        

        thus (( Op-XOR (( Op-XOR (u1,v1)),w1)) . i) = ((( Op-XOR (u1,v1)) . i) 'xor' (w1 . i)) by DESCIP_1:def 4, A3

        .= (((u1 . i) 'xor' (v1 . i)) 'xor' (w1 . i)) by DESCIP_1:def 4, A3

        .= ((u1 . i) 'xor' ((v1 . i) 'xor' (w1 . i))) by XBOOLEAN: 73

        .= ((u1 . i) 'xor' (( Op-XOR (v1,w1)) . i)) by DESCIP_1:def 4, A3

        .= (( Op-XOR (u1,( Op-XOR (v1,w1)))) . i) by DESCIP_1:def 4, A3;

      end;

      hence thesis by Lm1, A2, FINSEQ_1: 14;

    end;

    definition

      let n be non zero Element of NAT ;

      :: NBVECTSP:def1

      func XORB n -> BinOp of (n -tuples_on BOOLEAN ) means

      : Def1: for x,y be Element of (n -tuples_on BOOLEAN ) holds (it . (x,y)) = ( Op-XOR (x,y));

      existence

      proof

        deffunc F( Element of (n -tuples_on BOOLEAN ), Element of (n -tuples_on BOOLEAN )) = ( Op-XOR ($1,$2));

        consider f be Function of [:(n -tuples_on BOOLEAN ), (n -tuples_on BOOLEAN ):], (n -tuples_on BOOLEAN ) such that

         A1: for x,y be Element of (n -tuples_on BOOLEAN ) holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let H1,H2 be BinOp of (n -tuples_on BOOLEAN );

        assume

         A2: for x,y be Element of (n -tuples_on BOOLEAN ) holds (H1 . (x,y)) = ( Op-XOR (x,y));

        assume

         A3: for x,y be Element of (n -tuples_on BOOLEAN ) holds (H2 . (x,y)) = ( Op-XOR (x,y));

        for x,y be Element of (n -tuples_on BOOLEAN ) holds (H1 . (x,y)) = (H2 . (x,y))

        proof

          let x,y be Element of (n -tuples_on BOOLEAN );

          

          thus (H1 . (x,y)) = ( Op-XOR (x,y)) by A2

          .= (H2 . (x,y)) by A3;

        end;

        hence H1 = H2 by BINOP_1: 2;

      end;

    end

    definition

      let n be non zero Element of NAT ;

      :: NBVECTSP:def2

      func ZeroB n -> Element of (n -tuples_on BOOLEAN ) equals (n |-> 0 );

      correctness

      proof

        reconsider o = 0 as Element of BOOLEAN by TARSKI:def 2;

        (n |-> o) in (n -tuples_on BOOLEAN );

        hence thesis;

      end;

    end

    definition

      let n be non zero Element of NAT ;

      :: NBVECTSP:def3

      func n -BinaryGroup -> strict addLoopStr equals addLoopStr (# (n -tuples_on BOOLEAN ), ( XORB n), ( ZeroB n) #);

      correctness ;

    end

    theorem :: NBVECTSP:2

    

     Th2: for u1 be Element of (n -tuples_on BOOLEAN ) holds ( Op-XOR (u1,( ZeroB n))) = u1

    proof

      let u1 be Element of (n -tuples_on BOOLEAN );

      

       A1: ( len ( Op-XOR (u1,( ZeroB n)))) = n by Lm1;

      

       A2: ( len u1) = n by Lm1;

      now

        let i be Nat;

        assume 1 <= i & i <= ( len ( Op-XOR (u1,( ZeroB n))));

        then

         A3: i in ( Seg n) by A1;

        

        thus (( Op-XOR (u1,( ZeroB n))) . i) = ((u1 . i) 'xor' (( ZeroB n) . i)) by DESCIP_1:def 4, A3

        .= ((u1 . i) 'xor' FALSE )

        .= (u1 . i);

      end;

      hence thesis by Lm1, A2, FINSEQ_1: 14;

    end;

    theorem :: NBVECTSP:3

    

     Th3: for u1 be Element of (n -tuples_on BOOLEAN ) holds ( Op-XOR (u1,u1)) = ( ZeroB n)

    proof

      let u1 be Element of (n -tuples_on BOOLEAN );

      

       A1: ( len ( Op-XOR (u1,u1))) = n by Lm1;

      

       A2: ( len ( ZeroB n)) = n by Lm1;

      now

        let i be Nat;

        assume 1 <= i & i <= ( len ( Op-XOR (u1,u1)));

        then

         A3: i in ( Seg n) by A1;

        

        thus (( Op-XOR (u1,u1)) . i) = ((u1 . i) 'xor' (u1 . i)) by DESCIP_1:def 4, A3

        .= FALSE by XBOOLEAN: 147

        .= (( ZeroB n) . i);

      end;

      hence thesis by Lm1, A2, FINSEQ_1: 14;

    end;

    registration

      let n be non zero Element of NAT ;

      cluster (n -BinaryGroup ) -> add-associative right_zeroed right_complementable Abelian non empty;

      coherence

      proof

        set IT = (n -BinaryGroup );

        hereby

          let u,v,w be Element of IT;

          reconsider u1 = u, v1 = v, w1 = w as Element of (n -tuples_on BOOLEAN );

          

           A1: (u + v) = ( Op-XOR (u1,v1)) by Def1;

          

           A2: (v + w) = ( Op-XOR (v1,w1)) by Def1;

          

          thus ((u + v) + w) = ( Op-XOR (( Op-XOR (u1,v1)),w1)) by A1, Def1

          .= ( Op-XOR (u1,( Op-XOR (v1,w1)))) by Th1

          .= (u + (v + w)) by A2, Def1;

        end;

        hereby

          let v be Element of IT;

          reconsider v1 = v as Element of (n -tuples_on BOOLEAN );

          

          thus (v + ( 0. IT)) = ( Op-XOR (v1,( ZeroB n))) by Def1

          .= v by Th2;

        end;

        hereby

          let v be Element of IT;

          thus v is right_complementable

          proof

            reconsider v1 = v as Element of (n -tuples_on BOOLEAN );

            take v;

            

            thus (v + v) = ( Op-XOR (v1,v1)) by Def1

            .= ( 0. IT) by Th3;

          end;

        end;

        hereby

          let u,v be Element of IT;

          reconsider u1 = u, v1 = v as Element of (n -tuples_on BOOLEAN );

          

          thus (u + v) = ( Op-XOR (v1,u1)) by Def1

          .= (v + u) by Def1;

        end;

        thus thesis;

      end;

    end

    registration

      cluster -> boolean for Element of Z_2 ;

      coherence by BSPACE: 3;

    end

    registration

      let u,v be Element of Z_2 ;

      identify u 'xor' v with u + v;

      compatibility

      proof

        per cases by BSPACE: 5, BSPACE: 6, XBOOLEAN:def 3;

          suppose u = ( 0. Z_2 );

          hence thesis by RLVECT_1: 4, BSPACE: 5;

        end;

          suppose

           A1: u = ( 1. Z_2 );

          per cases by BSPACE: 5, BSPACE: 6, XBOOLEAN:def 3;

            suppose v = ( 0. Z_2 );

            hence thesis by RLVECT_1: 4, BSPACE: 5;

          end;

            suppose v = ( 1. Z_2 );

            hence thesis by A1, BSPACE: 5, BSPACE: 7, XBOOLEAN: 147;

          end;

        end;

      end;

      identify u '&' v with u * v;

      compatibility

      proof

        per cases by BSPACE: 5, BSPACE: 6, XBOOLEAN:def 3;

          suppose

           A2: u = ( 0. Z_2 );

          per cases by BSPACE: 5, BSPACE: 6, XBOOLEAN:def 3;

            suppose v = ( 0. Z_2 );

            

            then (u * v) = (( 0. Z_2 ) * ( 0. Z_2 ))

            .= 0 by BSPACE: 5;

            hence thesis by A2;

          end;

            suppose v = ( 1. Z_2 );

            (u * v) = (( 0. Z_2 ) * ( 1. Z_2 )) by A2

            .= 0 by BSPACE: 5;

            hence thesis by A2;

          end;

        end;

          suppose

           A3: u = ( 1. Z_2 );

          per cases by BSPACE: 5, BSPACE: 6, XBOOLEAN:def 3;

            suppose

             A4: v = ( 0. Z_2 );

            

            then (u * v) = (( 1. Z_2 ) * ( 0. Z_2 ))

            .= 0 by BSPACE: 5;

            hence thesis by A4;

          end;

            suppose v = ( 1. Z_2 );

            hence thesis by A3;

          end;

        end;

      end;

    end

    definition

      let n be non zero Element of NAT ;

      :: NBVECTSP:def4

      func MLTB n -> Function of [:the carrier of Z_2 , (n -tuples_on BOOLEAN ):], (n -tuples_on BOOLEAN ) means

      : Def4: for a be Element of BOOLEAN , x be Element of (n -tuples_on BOOLEAN ), i be set st i in ( Seg n) holds ((it . (a,x)) . i) = (a '&' (x . i));

      existence

      proof

        defpred P1[ boolean object, boolean-valued Function, boolean-valued Function] means for i be set st i in ( Seg n) holds ($3 . i) = ($1 '&' ($2 . i));

        

         A1: for a be Element of BOOLEAN holds for x be Element of (n -tuples_on BOOLEAN ) holds ex z be Element of (n -tuples_on BOOLEAN ) st P1[a, x, z]

        proof

          let a be Element of BOOLEAN , x be Element of (n -tuples_on BOOLEAN );

          deffunc H1( object) = (a '&' (x . $1));

          consider s be Function such that

           A2: ( dom s) = ( Seg n) and

           A3: for i be object st i in ( Seg n) holds (s . i) = H1(i) from FUNCT_1:sch 3;

           A4:

          now

            let y be object;

            assume y in ( rng s);

            then

            consider i be object such that

             A5: i in ( dom s) and

             A6: y = (s . i) by FUNCT_1:def 3;

            y = (a '&' (x . i)) by A2, A3, A5, A6;

            then (y = FALSE or y = TRUE ) by XBOOLEAN:def 3;

            hence y in BOOLEAN ;

          end;

          reconsider s as boolean-valued Function by A4, TARSKI:def 3, MARGREL1:def 16;

          s is Function of ( Seg n), BOOLEAN by A2, FUNCT_2: 2, TARSKI:def 3, A4;

          then s is Element of ( Funcs (( Seg n), BOOLEAN )) by FUNCT_2: 8;

          then

          reconsider s as Element of (n -tuples_on BOOLEAN ) by FINSEQ_2: 93;

          for i be set st i in ( Seg n) holds (s . i) = (a '&' (x . i)) by A3;

          hence thesis;

        end;

        ex f be Function of [: BOOLEAN , (n -tuples_on BOOLEAN ):], (n -tuples_on BOOLEAN ) st for a be Element of BOOLEAN holds for x be Element of (n -tuples_on BOOLEAN ) holds P1[a, x, (f . (a,x))] from BINOP_1:sch 3( A1);

        hence thesis by BSPACE: 3;

      end;

      uniqueness

      proof

        let f1,f2 be Function of [:the carrier of Z_2 , (n -tuples_on BOOLEAN ):], (n -tuples_on BOOLEAN );

        assume

         A7: for a be Element of BOOLEAN , x be Element of (n -tuples_on BOOLEAN ) holds for i be set st i in ( Seg n) holds ((f1 . (a,x)) . i) = (a '&' (x . i));

        assume

         A8: for a be Element of BOOLEAN , x be Element of (n -tuples_on BOOLEAN ) holds for i be set st i in ( Seg n) holds ((f2 . (a,x)) . i) = (a '&' (x . i));

        now

          let a be Element of the carrier of Z_2 , x be Element of (n -tuples_on BOOLEAN );

          

           A9: ( len (f1 . (a,x))) = n by CARD_1:def 7;

          

           A10: ( len (f2 . (a,x))) = n by CARD_1:def 7;

          now

            let i be Nat;

            assume 1 <= i & i <= ( len (f1 . (a,x)));

            then

             A11: i in ( Seg n) by A9;

            

            thus ((f1 . (a,x)) . i) = (a '&' (x . i)) by A7, A11, BSPACE: 3

            .= ((f2 . (a,x)) . i) by A8, A11, BSPACE: 3;

          end;

          hence (f1 . (a,x)) = (f2 . (a,x)) by FINSEQ_1: 14, CARD_1:def 7, A10;

        end;

        hence f1 = f2 by BINOP_1: 2;

      end;

    end

    definition

      let n be non zero Element of NAT ;

      :: NBVECTSP:def5

      func n -BinaryVectSp -> VectSp of Z_2 equals ModuleStr (# (n -tuples_on BOOLEAN ), ( XORB n), ( ZeroB n), ( MLTB n) #);

      correctness

      proof

        set X = Z_2 ;

        set X0 = (n -tuples_on BOOLEAN );

        set Z0 = ( ZeroB n);

        set ADD = ( XORB n);

        set LMLT = ( MLTB n);

        set XP = ModuleStr (# X0, ADD, Z0, LMLT #);

        reconsider 1X = TRUE as Element of Z_2 by BSPACE: 6;

        

         A1: XP is scalar-distributive vector-distributive scalar-associative scalar-unital

        proof

          thus XP is scalar-distributive

          proof

            let x,y be Element of X;

            let v be Element of XP;

            reconsider v1 = v as Element of (n -tuples_on BOOLEAN );

            reconsider xyv1 = ((x + y) * v) as Element of (n -tuples_on BOOLEAN );

            reconsider xv = (x * v) as Element of (n -tuples_on BOOLEAN );

            reconsider yv = (y * v) as Element of (n -tuples_on BOOLEAN );

            reconsider xyv2 = ((x * v) + (y * v)) as Element of (n -tuples_on BOOLEAN );

            

             A2: ( len xyv1) = n by CARD_1:def 7;

            

             A3: ( len xyv2) = n by CARD_1:def 7;

            now

              let i be Nat;

              assume 1 <= i & i <= ( len xyv1);

              then

               A4: i in ( Seg n) by A2;

              

               A5: (xv . i) = (x '&' (v1 . i)) by Def4, A4, BSPACE: 3;

              

               A6: (yv . i) = (y '&' (v1 . i)) by Def4, A4, BSPACE: 3;

              

              thus (xyv1 . i) = ((x 'xor' y) '&' (v1 . i)) by Def4, A4, BSPACE: 3

              .= ((xv . i) 'xor' (yv . i)) by XBOOLEAN: 75, A5, A6

              .= (( Op-XOR (xv,yv)) . i) by DESCIP_1:def 4, A4

              .= (xyv2 . i) by Def1;

            end;

            hence thesis by FINSEQ_1: 14, CARD_1:def 7, A3;

          end;

          thus XP is vector-distributive

          proof

            let x be Element of X;

            let v,w be Element of XP;

            reconsider v1 = v as Element of (n -tuples_on BOOLEAN );

            reconsider w1 = w as Element of (n -tuples_on BOOLEAN );

            reconsider xvw1 = (x * (v + w)) as Element of (n -tuples_on BOOLEAN );

            reconsider vw = (v + w) as Element of (n -tuples_on BOOLEAN );

            reconsider xv = (x * v) as Element of (n -tuples_on BOOLEAN );

            reconsider xw = (x * w) as Element of (n -tuples_on BOOLEAN );

            reconsider xvw2 = ((x * v) + (x * w)) as Element of (n -tuples_on BOOLEAN );

            

             A7: ( len xvw1) = n by CARD_1:def 7;

            

             A8: ( len xvw2) = n by CARD_1:def 7;

            now

              let i be Nat;

              assume 1 <= i & i <= ( len xvw1);

              then

               A9: i in ( Seg n) by A7;

              

               A10: (xv . i) = (x '&' (v1 . i)) by Def4, A9, BSPACE: 3;

              

               A11: (xw . i) = (x '&' (w1 . i)) by Def4, A9, BSPACE: 3;

              

               A12: (vw . i) = (( Op-XOR (v1,w1)) . i) by Def1

              .= ((v1 . i) 'xor' (w1 . i)) by DESCIP_1:def 4, A9;

              

              thus (xvw2 . i) = (( Op-XOR (xv,xw)) . i) by Def1

              .= ((x '&' (v1 . i)) 'xor' (x '&' (w1 . i))) by DESCIP_1:def 4, A9, A10, A11

              .= (x '&' (vw . i)) by XBOOLEAN: 75, A12

              .= (xvw1 . i) by Def4, A9, BSPACE: 3;

            end;

            hence thesis by FINSEQ_1: 14, CARD_1:def 7, A8;

          end;

          thus XP is scalar-associative

          proof

            let x,y be Element of X;

            let v be Element of XP;

            reconsider v1 = v as Element of (n -tuples_on BOOLEAN );

            reconsider xyv1 = ((x * y) * v) as Element of (n -tuples_on BOOLEAN );

            reconsider yv1 = (y * v) as Element of (n -tuples_on BOOLEAN );

            reconsider xyv2 = (x * (y * v)) as Element of (n -tuples_on BOOLEAN );

            

             A13: ( len xyv1) = n by CARD_1:def 7;

            

             A14: ( len xyv2) = n by CARD_1:def 7;

            now

              let i be Nat;

              assume 1 <= i & i <= ( len xyv1);

              then

               A15: i in ( Seg n) by A13;

              

               A16: (yv1 . i) = (y '&' (v1 . i)) by Def4, A15, BSPACE: 3;

              

              thus (xyv2 . i) = (x '&' (yv1 . i)) by Def4, A15, BSPACE: 3

              .= ((x '&' y) '&' (v1 . i)) by A16

              .= (xyv1 . i) by Def4, A15, BSPACE: 3;

            end;

            hence thesis by FINSEQ_1: 14, CARD_1:def 7, A14;

          end;

          thus XP is scalar-unital

          proof

            let v be Element of XP;

            reconsider v1 = v as Element of (n -tuples_on BOOLEAN );

            reconsider w1 = (( MLTB n) . (1X,v1)) as Element of (n -tuples_on BOOLEAN );

            

             A17: ( len v1) = n by CARD_1:def 7;

            

             A18: ( len w1) = n by CARD_1:def 7;

            now

              let i be Nat;

              assume 1 <= i & i <= ( len v1);

              then i in ( Seg n) by A17;

              

              hence (w1 . i) = ( TRUE '&' (v1 . i)) by Def4

              .= (v1 . i);

            end;

            hence thesis by FINSEQ_1: 14, CARD_1:def 7, A18, BSPACE: 6;

          end;

        end;

        

         A19: XP is add-associative

        proof

          for u,v,w be Element of XP holds ((u + v) + w) = (u + (v + w))

          proof

            let u,v,w be Element of XP;

            reconsider u1 = u, v1 = v, w1 = w as Element of (n -tuples_on BOOLEAN );

            

             A20: (u + v) = ( Op-XOR (u1,v1)) by Def1;

            

             A21: (v + w) = ( Op-XOR (v1,w1)) by Def1;

            

            thus ((u + v) + w) = ( Op-XOR (( Op-XOR (u1,v1)),w1)) by A20, Def1

            .= ( Op-XOR (u1,( Op-XOR (v1,w1)))) by Th1

            .= (u + (v + w)) by A21, Def1;

          end;

          hence thesis by RLVECT_1:def 3;

        end;

        

         A22: XP is right_zeroed

        proof

          for v be Element of XP holds (v + ( 0. XP)) = v

          proof

            let v be Element of XP;

            reconsider v1 = v as Element of (n -tuples_on BOOLEAN );

            

            thus (v + ( 0. XP)) = ( Op-XOR (v1,( ZeroB n))) by Def1

            .= v by Th2;

          end;

          hence thesis by RLVECT_1:def 4;

        end;

        

         A23: XP is right_complementable

        proof

          for x be Element of XP holds x is right_complementable

          proof

            let v be Element of XP;

            ex y be Element of XP st (v + y) = ( 0. XP)

            proof

              reconsider v1 = v as Element of (n -tuples_on BOOLEAN );

              take v;

              

              thus (v + v) = ( Op-XOR (v1,v1)) by Def1

              .= ( 0. XP) by Th3;

            end;

            hence thesis by ALGSTR_0:def 11;

          end;

          hence thesis by ALGSTR_0:def 16;

        end;

        XP is Abelian

        proof

          for v,w be Element of XP holds (v + w) = (w + v)

          proof

            let u,v be Element of XP;

            reconsider u1 = u, v1 = v as Element of (n -tuples_on BOOLEAN );

            

            thus (u + v) = ( Op-XOR (v1,u1)) by Def1

            .= (v + u) by Def1;

          end;

          hence thesis by RLVECT_1:def 2;

        end;

        hence thesis by A1, A19, A22, A23;

      end;

    end

    registration

      let n be non zero Element of NAT ;

      cluster (n -BinaryVectSp ) -> finite;

      coherence ;

    end

    registration

      let n be non zero Element of NAT ;

      cluster -> finite for Subspace of (n -BinaryVectSp );

      coherence

      proof

        let V be Subspace of (n -BinaryVectSp );

        the carrier of V c= the carrier of (n -BinaryVectSp ) by VECTSP_4:def 2;

        hence thesis;

      end;

    end

    theorem :: NBVECTSP:4

    

     Th4: for n be Nat holds ( Sum (n |-> ( 0. Z_2 ))) = ( 0. Z_2 )

    proof

      let n be Nat;

      set x = (n |-> ( 0. Z_2 ));

      

       A1: ( len x) = ( len x);

      now

        let k be Nat;

        assume k in ( dom x);

        

        then (x /. k) = (x . k) by PARTFUN1:def 6

        .= ( 0. Z_2 ) by BSPACE: 5;

        hence (x . k) = ((x /. k) + (x /. k)) by BSPACE: 5;

      end;

      then

       A2: (( Sum x) - ( Sum x)) = ((( Sum x) + ( Sum x)) - ( Sum x)) by A1, RLVECT_2: 2;

      ((( Sum x) + ( Sum x)) - ( Sum x)) = (( Sum x) + (( Sum x) - ( Sum x))) by RLVECT_1: 28

      .= (( Sum x) + ( 0. Z_2 )) by RLVECT_1: 15

      .= ( Sum x) by BSPACE: 5;

      hence thesis by A2, RLVECT_1: 15;

    end;

    theorem :: NBVECTSP:5

    

     Th5: for x be FinSequence of Z_2 , v be Element of Z_2 , j be Nat st ( len x) = m & j in ( Seg m) & for i be Nat st i in ( Seg m) holds (i = j implies (x . i) = v) & (i <> j implies (x . i) = ( 0. Z_2 )) holds ( Sum x) = v

    proof

      defpred P[ Nat] means for m be non zero Element of NAT , x be FinSequence of Z_2 , v be Element of Z_2 , j be Nat st $1 = m & ( len x) = m & j in ( Seg m) & for i be Nat st i in ( Seg m) holds (i = j implies (x . i) = v) & (i <> j implies (x . i) = ( 0. Z_2 )) holds ( Sum x) = v;

      

       A1: P[ 0 ];

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        for m be non zero Element of NAT , x be FinSequence of Z_2 , v be Element of Z_2 , j be Nat st (k + 1) = m & ( len x) = m & j in ( Seg m) & for i be Nat st i in ( Seg m) holds (i = j implies (x . i) = v) & (i <> j implies (x . i) = ( 0. Z_2 )) holds ( Sum x) = v

        proof

          let m be non zero Element of NAT , x be FinSequence of Z_2 , v be Element of Z_2 , j be Nat;

          assume

           A4: (k + 1) = m & ( len x) = m & j in ( Seg m) & for i be Nat st i in ( Seg m) holds (i = j implies (x . i) = v) & (i <> j implies (x . i) = ( 0. Z_2 ));

          reconsider xk = (x | k) as FinSequence of Z_2 ;

          

           A5: k <= (k + 1) by NAT_1: 11;

          

           A6: ( len xk) = k by A4, NAT_1: 11, FINSEQ_1: 59;

          

           A7: ( len x) = (( len xk) + 1) by A4, NAT_1: 11, FINSEQ_1: 59;

          

           A8: xk = (x | ( dom xk)) by A6, FINSEQ_1:def 3;

          

           A9: ( len (( len xk) |-> ( 0. Z_2 ))) = ( len xk) by CARD_1:def 7;

          per cases ;

            suppose

             A10: j = m;

            then

             A11: (x . ( len x)) = v by A4;

            for i be Nat st i in ( dom xk) holds (xk . i) = ((( len xk) |-> ( 0. Z_2 )) . i)

            proof

              let i be Nat;

              assume

               A12: i in ( dom xk);

              then

               A13: i in ( Seg k) by A6, FINSEQ_1:def 3;

              then

               A14: i in ( Seg m) by A4, A5, FINSEQ_1: 5, TARSKI:def 3;

              1 <= i & i <= k by FINSEQ_1: 1, A13;

              then i <> j by A4, A10, NAT_1: 13;

              then (x . i) = ( 0. Z_2 ) by A4, A14;

              then (xk . i) = ( 0. Z_2 ) by A12, A8, FUNCT_1: 49;

              hence thesis by BSPACE: 5;

            end;

            then

             A15: xk = (( len xk) |-> ( 0. Z_2 )) by A9, FINSEQ_2: 9;

            

            thus ( Sum x) = (( Sum xk) + v) by RLVECT_1: 38, A7, A8, A11

            .= (v + ( 0. Z_2 )) by A15, Th4

            .= v by BSPACE: 5;

          end;

            suppose

             A16: j <> m;

            

             A17: 1 <= j & j <= m by A4, FINSEQ_1: 1;

            then j < m by A16, XXREAL_0: 1;

            then j <= k by A4, NAT_1: 13;

            then

             A18: j in ( Seg k) by A17;

            

             A19: k <> 0 by A4, A16, XXREAL_0: 1, A17;

            for i be Nat st i in ( Seg k) holds (i = j implies (xk . i) = v) & (i <> j implies (xk . i) = ( 0. Z_2 ))

            proof

              let i be Nat;

              assume

               A20: i in ( Seg k);

              

               A21: ( Seg k) c= ( Seg m) by A4, NAT_1: 11, FINSEQ_1: 5;

              (xk . i) = (x . i) by A20, FUNCT_1: 49;

              hence (i = j implies (xk . i) = v) & (i <> j implies (xk . i) = ( 0. Z_2 )) by A4, A20, A21;

            end;

            then

             A22: ( Sum xk) = v by A6, A3, A18, A19;

            

             A23: m in ( Seg m) by FINSEQ_1: 3;

            

             A24: (x . ( len x)) = ( 0. Z_2 ) by A4, A23, A16;

            

            thus ( Sum x) = (v + ( 0. Z_2 )) by RLVECT_1: 38, A7, A8, A24, A22

            .= v by BSPACE: 5;

          end;

        end;

        hence thesis;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: NBVECTSP:6

    

     Th6: for L be the carrier of (n -BinaryVectSp ) -valued FinSequence, j be Nat st ( len L) = m & m <= n & j in ( Seg n) holds ex x be FinSequence of Z_2 st ( len x) = m & for i be Nat st i in ( Seg m) holds ex K be Element of (n -tuples_on BOOLEAN ) st K = (L . i) & (x . i) = (K . j)

    proof

      let L be the carrier of (n -BinaryVectSp ) -valued FinSequence, j be Nat;

      assume

       A1: ( len L) = m & m <= n & j in ( Seg n);

      defpred P1[ Nat, set] means ex K be Element of (n -tuples_on BOOLEAN ) st K = (L . $1) & $2 = (K . j);

      

       A2: for i be Nat st i in ( Seg m) holds ex y be Element of BOOLEAN st P1[i, y]

      proof

        let i be Nat;

        assume i in ( Seg m);

        then i in ( dom L) by A1, FINSEQ_1:def 3;

        then (L /. i) = (L . i) by PARTFUN1:def 6;

        then

        reconsider K = (L . i) as Element of (n -tuples_on BOOLEAN );

        take (K . j);

        thus P1[i, (K . j)];

      end;

      consider x be FinSequence of BOOLEAN such that

       A3: ( dom x) = ( Seg m) & for i be Nat st i in ( Seg m) holds P1[i, (x . i)] from FINSEQ_1:sch 5( A2);

      ( len x) = m by FINSEQ_1:def 3, A3;

      hence thesis by A3, BSPACE: 3;

    end;

    theorem :: NBVECTSP:7

    

     Th7: for L be the carrier of (n -BinaryVectSp ) -valued FinSequence, Suml be Element of (n -tuples_on BOOLEAN ), j be Nat st ( len L) = m & m <= n & Suml = ( Sum L) & j in ( Seg n) holds ex x be FinSequence of Z_2 st ( len x) = m & (Suml . j) = ( Sum x) & for i be Nat st i in ( Seg m) holds ex K be Element of (n -tuples_on BOOLEAN ) st K = (L . i) & (x . i) = (K . j)

    proof

      let L be the carrier of (n -BinaryVectSp ) -valued FinSequence, Suml be Element of (n -tuples_on BOOLEAN ), j be Nat;

      assume

       A1: ( len L) = m & m <= n & Suml = ( Sum L) & j in ( Seg n);

      then

      consider x be FinSequence of Z_2 such that

       A2: ( len x) = m & for i be Nat st i in ( Seg m) holds ex K be Element of (n -tuples_on BOOLEAN ) st K = (L . i) & (x . i) = (K . j) by Th6;

      consider f be Function of NAT , (n -BinaryVectSp ) such that

       A3: ( Sum L) = (f . ( len L)) & (f . 0 ) = ( 0. (n -BinaryVectSp )) & (for j be Nat holds for v be Element of (n -BinaryVectSp ) st j < ( len L) & v = (L . (j + 1)) holds (f . (j + 1)) = ((f . j) + v)) by RLVECT_1:def 12;

      defpred P1[ Nat, set] means ex K be Element of (n -tuples_on BOOLEAN ) st K = (f . $1) & $2 = (K . j);

      

       A4: for i be Element of NAT holds ex y be Element of the carrier of Z_2 st P1[i, y]

      proof

        let i be Element of NAT ;

        reconsider K = (f . i) as Element of (n -tuples_on BOOLEAN );

        reconsider y = (K . j) as Element of Z_2 by BSPACE: 3;

        take y;

        thus P1[i, y];

      end;

      consider g be Function of NAT , Z_2 such that

       A5: for i be Element of NAT holds P1[i, (g . i)] from FUNCT_2:sch 3( A4);

      set Sumlj = (Suml . j);

      

       A6: Sumlj = (g . ( len x))

      proof

        ex K be Element of (n -tuples_on BOOLEAN ) st K = (f . ( len L)) & (g . ( len L)) = (K . j) by A5;

        hence Sumlj = (g . ( len x)) by A1, A3, A2;

      end;

      

       A7: (g . 0 ) = ( 0. Z_2 )

      proof

        ex K be Element of (n -tuples_on BOOLEAN ) st K = (f . 0 ) & (g . 0 ) = (K . j) by A5;

        hence (g . 0 ) = ( 0. Z_2 ) by A3, BSPACE: 5;

      end;

      

       A8: for k be Nat holds for vj be Element of Z_2 st k < ( len x) & vj = (x . (k + 1)) holds (g . (k + 1)) = ((g . k) + vj)

      proof

        let k be Nat, vj be Element of Z_2 ;

        assume

         A9: k < ( len x) & vj = (x . (k + 1));

        then 1 <= (k + 1) & (k + 1) <= ( len x) by NAT_1: 11, NAT_1: 13;

        then (k + 1) in ( Seg m) by A2;

        then

        consider LVn be Element of (n -tuples_on BOOLEAN ) such that

         A10: LVn = (L . (k + 1)) & (x . (k + 1)) = (LVn . j) by A2;

        reconsider Vn = LVn as Element of (n -BinaryVectSp );

        consider K1 be Element of (n -tuples_on BOOLEAN ) such that

         A11: K1 = (f . (k + 1)) & (g . (k + 1)) = (K1 . j) by A5;

        reconsider VK1 = K1 as Element of (n -BinaryVectSp );

        for i be Nat holds P1[i, (g . i)]

        proof

          let i be Nat;

          i is Element of NAT by ORDINAL1:def 12;

          hence thesis by A5;

        end;

        then

        consider K0 be Element of (n -tuples_on BOOLEAN ) such that

         A12: K0 = (f . k) & (g . k) = (K0 . j);

        reconsider VK0 = K0 as Element of (n -BinaryVectSp );

        (VK0 + Vn) = ( Op-XOR (K0,LVn)) by Def1;

        hence (g . (k + 1)) = ((g . k) + vj) by A11, A3, A9, A10, A1, A2, A12, DESCIP_1:def 4;

      end;

      (Suml . j) = ( Sum x) by A6, A7, A8, RLVECT_1:def 12;

      hence thesis by A2;

    end;

    theorem :: NBVECTSP:8

    

     Th8: m <= n implies ex A be FinSequence of (n -tuples_on BOOLEAN ) st ( len A) = m & A is one-to-one & ( card ( rng A)) = m & (for i,j be Nat st i in ( Seg m) & j in ( Seg n) holds (i = j implies ((A . i) . j) = TRUE ) & (i <> j implies ((A . i) . j) = FALSE ))

    proof

      assume

       A1: m <= n;

      defpred P[ Nat, Function] means for j be Nat st j in ( Seg n) holds ($1 = j implies ($2 . j) = TRUE ) & ($1 <> j implies ($2 . j) = FALSE );

      

       A2: for k be Nat st k in ( Seg m) holds ex x be Element of (n -tuples_on BOOLEAN ) st P[k, x]

      proof

        let k be Nat;

        assume k in ( Seg m);

        defpred P1[ Nat, set] means (k = $1 implies $2 = TRUE ) & (k <> $1 implies $2 = FALSE );

        

         A3: for j be Nat st j in ( Seg n) holds ex y be Element of BOOLEAN st P1[j, y]

        proof

          let j be Nat;

          assume j in ( Seg n);

          per cases ;

            suppose

             A4: k = j;

            take TRUE ;

            thus P1[j, TRUE ] by A4;

          end;

            suppose

             A5: k <> j;

            take FALSE ;

            thus P1[j, FALSE ] by A5;

          end;

        end;

        consider x be FinSequence of BOOLEAN such that

         A6: ( dom x) = ( Seg n) & for j be Nat st j in ( Seg n) holds P1[j, (x . j)] from FINSEQ_1:sch 5( A3);

        reconsider x as Element of ( BOOLEAN * ) by FINSEQ_1:def 11;

        ( len x) = n by A6, FINSEQ_1:def 3;

        then x in { s where s be Element of ( BOOLEAN * ) : ( len s) = n };

        then

        reconsider x as Element of (n -tuples_on BOOLEAN );

        take x;

        thus P[k, x] by A6;

      end;

      consider A be FinSequence of (n -tuples_on BOOLEAN ) such that

       A7: ( dom A) = ( Seg m) & for k be Nat st k in ( Seg m) holds P[k, (A . k)] from FINSEQ_1:sch 5( A2);

      take A;

      thus ( len A) = m by A7, FINSEQ_1:def 3;

      

       A8: for x,y be object st x in ( dom A) & y in ( dom A) & (A . x) = (A . y) holds x = y

      proof

        let x,y be object;

        assume

         A9: x in ( dom A) & y in ( dom A) & (A . x) = (A . y);

        then

        reconsider i1 = x, i2 = y as Nat;

        assume

         A10: x <> y;

        

         A11: ( Seg m) c= ( Seg n) by A1, FINSEQ_1: 5;

        ((A . i2) . i1) = FALSE by A10, A9, A7, A11;

        hence contradiction by A9, A7, A11;

      end;

      hence A is one-to-one by FUNCT_1:def 4;

      

       A12: ( card ( dom A)) = m by FINSEQ_1: 57, A7;

      (( dom A),( rng A)) are_equipotent by A8, FUNCT_1:def 4, WELLORD2:def 4;

      hence ( card ( rng A)) = m by A12, CARD_1: 5;

      thus thesis by A7;

    end;

    theorem :: NBVECTSP:9

    

     Th9: for A be FinSequence of (n -tuples_on BOOLEAN ), B be finite Subset of (n -BinaryVectSp ), l be Linear_Combination of B, Suml be Element of (n -tuples_on BOOLEAN ) st ( rng A) = B & m <= n & ( len A) = m & Suml = ( Sum l) & A is one-to-one & (for i,j be Nat st i in ( Seg n) & j in ( Seg m) holds (i = j implies ((A . i) . j) = TRUE ) & (i <> j implies ((A . i) . j) = FALSE )) holds for j be Nat st j in ( Seg m) holds (Suml . j) = (l . (A . j))

    proof

      let A be FinSequence of (n -tuples_on BOOLEAN ), B be finite Subset of (n -BinaryVectSp ), l be Linear_Combination of B, Suml be Element of (n -tuples_on BOOLEAN );

      assume that

       A1: ( rng A) = B and

       A2: m <= n and

       A3: ( len A) = m and

       A4: Suml = ( Sum l) and

       A5: A is one-to-one and

       A6: for i,j be Nat st i in ( Seg n) & j in ( Seg m) holds (i = j implies ((A . i) . j) = TRUE ) & (i <> j implies ((A . i) . j) = FALSE );

      set V = (n -BinaryVectSp );

      let j be Nat;

      assume

       A7: j in ( Seg m);

      reconsider FA = A as FinSequence of V;

      

       A8: j in ( Seg n) by A7, A2, FINSEQ_1: 5, TARSKI:def 3;

      

       A9: ( Carrier l) c= ( rng FA) by A1, VECTSP_6:def 4;

      

       A10: ( len (l (#) FA)) = m by A3, VECTSP_6:def 5;

      Suml = ( Sum (l (#) FA)) by VECTSP_9: 3, A5, A9, A4;

      then

      consider x be FinSequence of Z_2 such that

       A11: ( len x) = m & (Suml . j) = ( Sum x) & for i be Nat st i in ( Seg m) holds ex K be Element of (n -tuples_on BOOLEAN ) st K = ((l (#) FA) . i) & (x . i) = (K . j) by Th7, A2, A8, A10;

      

       A12: for i be Nat st i in ( Seg m) holds (i = j implies (x . i) = (l . (A . j))) & (i <> j implies (x . i) = ( 0. Z_2 ))

      proof

        let i be Nat;

        assume

         A13: i in ( Seg m);

        then

        consider K be Element of (n -tuples_on BOOLEAN ) such that

         A14: K = ((l (#) FA) . i) & (x . i) = (K . j) by A11;

        

         A15: i in ( Seg n) by A13, A2, FINSEQ_1: 5, TARSKI:def 3;

        

         A16: i in ( dom (l (#) FA)) by FINSEQ_1:def 3, A13, A10;

        

         A17: K = ((l . (FA /. i)) * (FA /. i)) by A14, A16, VECTSP_6:def 5;

        reconsider FAi = (FA /. i) as Element of (n -tuples_on BOOLEAN );

        set lFAi = (l . (FA /. i));

        

         A18: (K . j) = (lFAi '&' (FAi . j)) by Def4, A8, A17, BSPACE: 3;

        

         A19: i in ( dom A) by A3, FINSEQ_1:def 3, A13;

        then

         A20: (FAi . j) = ((A . i) . j) by PARTFUN1:def 6;

        thus i = j implies (x . i) = (l . (A . j))

        proof

          assume

           A21: i = j;

          then (K . j) = (lFAi '&' TRUE ) by A6, A8, A13, A18, A20;

          hence (x . i) = (l . (A . j)) by A21, A14, A19, PARTFUN1:def 6;

        end;

        assume i <> j;

        then (K . j) = (lFAi '&' FALSE ) by A6, A7, A15, A18, A20;

        hence (x . i) = ( 0. Z_2 ) by A14, BSPACE: 5;

      end;

      j in ( dom A) by A3, A7, FINSEQ_1:def 3;

      then (l . (A . j)) is Element of Z_2 by PARTFUN1: 4, FUNCT_2: 5;

      hence thesis by Th5, A7, A11, A12;

    end;

    theorem :: NBVECTSP:10

    

     Th10: for A be FinSequence of (n -tuples_on BOOLEAN ), B be finite Subset of (n -BinaryVectSp ) st ( rng A) = B & m <= n & ( len A) = m & A is one-to-one & (for i,j be Nat st i in ( Seg n) & j in ( Seg m) holds (i = j implies ((A . i) . j) = TRUE ) & (i <> j implies ((A . i) . j) = FALSE )) holds B is linearly-independent

    proof

      let A be FinSequence of (n -tuples_on BOOLEAN ), B be finite Subset of (n -BinaryVectSp );

      assume that

       A1: ( rng A) = B and

       A2: m <= n and

       A3: ( len A) = m and

       A4: A is one-to-one and

       A5: for i,j be Nat st i in ( Seg n) & j in ( Seg m) holds (i = j implies ((A . i) . j) = TRUE ) & (i <> j implies ((A . i) . j) = FALSE );

      set V = (n -BinaryVectSp );

      for l be Linear_Combination of B st ( Sum l) = ( 0. V) holds ( Carrier l) = {}

      proof

        let l be Linear_Combination of B;

        assume

         A6: ( Sum l) = ( 0. V);

        assume ( Carrier l) <> {} ;

        then

        consider x be object such that

         A7: x in ( Carrier l) by XBOOLE_0:def 1;

        consider v be Element of V such that

         A8: x = v & (l . v) <> ( 0. Z_2 ) by A7;

        

         A9: ( Carrier l) c= B by VECTSP_6:def 4;

        reconsider Suml = ( Sum l) as Element of (n -tuples_on BOOLEAN );

        consider j be object such that

         A10: j in ( dom A) & v = (A . j) by A1, A9, A7, A8, FUNCT_1:def 3;

        

         A11: j in ( Seg m) by A3, A10, FINSEQ_1:def 3;

        reconsider j as Nat by A10;

        (Suml . j) = (l . (A . j)) by Th9, A1, A2, A3, A4, A5, A11;

        hence contradiction by A6, A8, A10, BSPACE: 5;

      end;

      hence thesis by VECTSP_7:def 1;

    end;

    theorem :: NBVECTSP:11

    

     Th11: for A be FinSequence of (n -tuples_on BOOLEAN ), B be finite Subset of (n -BinaryVectSp ), v be Element of (n -tuples_on BOOLEAN ) st ( rng A) = B & ( len A) = n & A is one-to-one holds ex l be Linear_Combination of B st for j be Nat st j in ( Seg n) holds (v . j) = (l . (A . j))

    proof

      let A be FinSequence of (n -tuples_on BOOLEAN ), B be finite Subset of (n -BinaryVectSp ), v be Element of (n -tuples_on BOOLEAN );

      assume that

       A1: ( rng A) = B and

       A2: ( len A) = n and

       A3: A is one-to-one;

      set V = (n -BinaryVectSp );

      defpred P1[ object, object] means ex j be Nat st j in ( Seg n) & $1 = (A . j) & $2 = (v . j);

      

       A4: for x be object st x in B holds ex y be object st y in the carrier of Z_2 & P1[x, y]

      proof

        let x be object;

        assume

         A5: x in B;

        consider j be object such that

         A6: j in ( dom A) & x = (A . j) by A1, A5, FUNCT_1:def 3;

        

         A7: j in ( Seg n) by A2, A6, FINSEQ_1:def 3;

        reconsider j as Nat by A6;

        (v . j) in the carrier of Z_2 by BSPACE: 3;

        hence thesis by A6, A7;

      end;

      consider l0 be Function of B, the carrier of Z_2 such that

       A8: for x be object st x in B holds P1[x, (l0 . x)] from FUNCT_2:sch 1( A4);

      

       A9: for j be Nat st j in ( Seg n) holds (l0 . (A . j)) = (v . j)

      proof

        let j be Nat;

        assume j in ( Seg n);

        then

         A10: j in ( dom A) by A2, FINSEQ_1:def 3;

        then

        consider i be Nat such that

         A11: i in ( Seg n) & (A . j) = (A . i) & (l0 . (A . j)) = (v . i) by A1, FUNCT_1: 3, A8;

        i in ( dom A) by A2, A11, FINSEQ_1:def 3;

        hence (l0 . (A . j)) = (v . j) by A3, A10, A11, FUNCT_1:def 4;

      end;

      set f = (the carrier of V --> ( 0. Z_2 ));

      set l = (f +* l0);

      

       A12: ( dom l) = (( dom f) \/ ( dom l0)) by FUNCT_4:def 1

      .= (the carrier of V \/ ( dom l0))

      .= (the carrier of V \/ B) by FUNCT_2:def 1

      .= the carrier of V by XBOOLE_1: 12;

      ( rng l) c= the carrier of Z_2 ;

      then l is Function of the carrier of V, the carrier of Z_2 by FUNCT_2: 2, A12;

      then

      reconsider l as Element of ( Funcs (the carrier of V,the carrier of Z_2 )) by FUNCT_2: 8;

      

       A13: for v be Element of V st not v in B holds (l . v) = ( 0. Z_2 )

      proof

        let v be Element of V;

        v in ( dom l) by A12;

        then

         A14: v in (( dom f) \/ ( dom l0)) by FUNCT_4:def 1;

        assume not v in B;

        then not v in ( dom l0);

        then (l . v) = (f . v) by A14, FUNCT_4:def 1;

        hence (l . v) = ( 0. Z_2 );

      end;

      then

      reconsider l as Linear_Combination of V by VECTSP_6:def 1;

      for x be object st x in ( Carrier l) holds x in B

      proof

        let x be object;

        assume x in ( Carrier l);

        then ex v be Element of V st x = v & (l . v) <> ( 0. Z_2 );

        hence x in B by A13;

      end;

      then

       A15: l is Linear_Combination of B by TARSKI:def 3, VECTSP_6:def 4;

      for j be Nat st j in ( Seg n) holds (v . j) = (l . (A . j))

      proof

        let j be Nat;

        assume

         A16: j in ( Seg n);

        then j in ( dom A) by A2, FINSEQ_1:def 3;

        then

         A17: (A . j) in B by A1, FUNCT_1: 3;

        then

        reconsider x = (A . j) as Element of V;

        

         A18: x in ( dom l0) by FUNCT_2:def 1, A17;

        x in ( dom l) by A12;

        then

         A19: x in (( dom f) \/ ( dom l0)) by FUNCT_4:def 1;

        

        thus (l . (A . j)) = (l0 . x) by A18, A19, FUNCT_4:def 1

        .= (v . j) by A9, A16;

      end;

      hence thesis by A15;

    end;

    theorem :: NBVECTSP:12

    

     Th12: for A be FinSequence of (n -tuples_on BOOLEAN ), B be finite Subset of (n -BinaryVectSp ) st ( rng A) = B & ( len A) = n & A is one-to-one & (for i,j be Nat st i in ( Seg n) & j in ( Seg n) holds (i = j implies ((A . i) . j) = TRUE ) & (i <> j implies ((A . i) . j) = FALSE )) holds ( Lin B) = ModuleStr (# the carrier of (n -BinaryVectSp ), the addF of (n -BinaryVectSp ), the ZeroF of (n -BinaryVectSp ), the lmult of (n -BinaryVectSp ) #)

    proof

      let A be FinSequence of (n -tuples_on BOOLEAN ), B be finite Subset of (n -BinaryVectSp );

      assume that

       A1: ( rng A) = B and

       A2: ( len A) = n and

       A3: A is one-to-one and

       A4: for i,j be Nat st i in ( Seg n) & j in ( Seg n) holds (i = j implies ((A . i) . j) = TRUE ) & (i <> j implies ((A . i) . j) = FALSE );

      set V = (n -BinaryVectSp );

      for x be object holds x in the carrier of ( Lin B) iff x in the carrier of V

      proof

        let x be object;

        hereby

          assume

           A5: x in the carrier of ( Lin B);

          the carrier of ( Lin B) c= the carrier of V by VECTSP_4:def 2;

          hence x in the carrier of V by A5;

        end;

        assume x in the carrier of V;

        then

        reconsider v = x as Element of (n -tuples_on BOOLEAN );

        consider l be Linear_Combination of B such that

         A6: for j be Nat st j in ( Seg n) holds (v . j) = (l . (A . j)) by Th11, A1, A2, A3;

        reconsider Suml = ( Sum l) as Element of (n -tuples_on BOOLEAN );

        

         A7: ( len v) = n by Lm1;

        

         A8: ( len Suml) = n by Lm1;

        

         A9: ( dom v) = ( Seg n) by FINSEQ_1:def 3, A7

        .= ( dom Suml) by FINSEQ_1:def 3, A8;

        for j be Nat st j in ( dom v) holds (v . j) = (Suml . j)

        proof

          let j be Nat;

          assume j in ( dom v);

          then

           A10: j in ( Seg n) by FINSEQ_1:def 3, A7;

          

          thus (v . j) = (l . (A . j)) by A6, A10

          .= (Suml . j) by Th9, A1, A2, A3, A4, A10;

        end;

        then x in ( Lin B) by FINSEQ_1: 13, A9, VECTSP_7: 7;

        hence x in the carrier of ( Lin B) by STRUCT_0:def 5;

      end;

      hence thesis by TARSKI: 2, VECTSP_4: 31;

    end;

    theorem :: NBVECTSP:13

    

     Th13: ex B be finite Subset of (n -BinaryVectSp ) st B is Basis of (n -BinaryVectSp ) & ( card B) = n & ex A be FinSequence of (n -tuples_on BOOLEAN ) st ( len A) = n & A is one-to-one & ( card ( rng A)) = n & ( rng A) = B & (for i,j be Nat st i in ( Seg n) & j in ( Seg n) holds (i = j implies ((A . i) . j) = TRUE ) & (i <> j implies ((A . i) . j) = FALSE ))

    proof

      set V = (n -BinaryVectSp );

      consider A be FinSequence of (n -tuples_on BOOLEAN ) such that

       A1: ( len A) = n & A is one-to-one & ( card ( rng A)) = n & (for i,j be Nat st i in ( Seg n) & j in ( Seg n) holds (i = j implies ((A . i) . j) = TRUE ) & (i <> j implies ((A . i) . j) = FALSE )) by Th8;

      reconsider B = ( rng A) as finite Subset of (n -BinaryVectSp );

      

       A2: B is linearly-independent by A1, Th10;

      ( Lin B) = ModuleStr (# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by A1, Th12;

      then B is Basis of V by VECTSP_7:def 3, A2;

      hence thesis by A1;

    end;

    theorem :: NBVECTSP:14

    

     Th14: (n -BinaryVectSp ) is finite-dimensional & ( dim (n -BinaryVectSp )) = n

    proof

      set V = (n -BinaryVectSp );

      consider B be finite Subset of (n -BinaryVectSp ) such that

       A1: B is Basis of (n -BinaryVectSp ) & ( card B) = n & ex A be FinSequence of (n -tuples_on BOOLEAN ) st ( len A) = n & A is one-to-one & ( card ( rng A)) = n & ( rng A) = B & for i,j be Nat st i in ( Seg n) & j in ( Seg n) holds (i = j implies ((A . i) . j) = TRUE ) & (i <> j implies ((A . i) . j) = FALSE ) by Th13;

      thus V is finite-dimensional by A1, MATRLIN:def 1;

      hence ( dim V) = n by A1, VECTSP_9:def 1;

    end;

    registration

      let n be non zero Element of NAT ;

      cluster (n -BinaryVectSp ) -> finite-dimensional;

      coherence by Th14;

    end

    theorem :: NBVECTSP:15

    for A be FinSequence of (n -tuples_on BOOLEAN ), C be Subset of (n -BinaryVectSp ) st ( len A) = n & A is one-to-one & ( card ( rng A)) = n & (for i,j be Nat st i in ( Seg n) & j in ( Seg n) holds (i = j implies ((A . i) . j) = TRUE ) & (i <> j implies ((A . i) . j) = FALSE )) & C c= ( rng A) holds ( Lin C) is Subspace of (n -BinaryVectSp ) & C is Basis of ( Lin C) & ( dim ( Lin C)) = ( card C)

    proof

      let A be FinSequence of (n -tuples_on BOOLEAN ), C be Subset of (n -BinaryVectSp );

      assume

       A1: ( len A) = n & A is one-to-one & ( card ( rng A)) = n & (for i,j be Nat st i in ( Seg n) & j in ( Seg n) holds (i = j implies ((A . i) . j) = TRUE ) & (i <> j implies ((A . i) . j) = FALSE ));

      assume

       A2: C c= ( rng A);

      reconsider B = ( rng A) as finite Subset of (n -BinaryVectSp );

      B is linearly-independent by A1, Th10;

      then

       A3: C is linearly-independent by A2, VECTSP_7: 1;

      for x be object st x in C holds x in the carrier of ( Lin C) by VECTSP_7: 8, STRUCT_0:def 5;

      then

      reconsider C0 = C as Subset of ( Lin C) by TARSKI:def 3;

      ( Lin C0) = the ModuleStr of ( Lin C) by VECTSP_9: 17;

      then C0 is Basis of ( Lin C) by VECTSP_7:def 3, A3, VECTSP_9: 12;

      hence thesis by VECTSP_9:def 1;

    end;