bspace.miz

    begin

    definition

      let S be 1-sorted;

      :: BSPACE:def1

      func <*> S -> FinSequence of S equals ( <*> ( [#] S));

      coherence ;

    end

    reserve S for 1-sorted,

i for Element of NAT ,

p for FinSequence,

X for set;

    theorem :: BSPACE:1

    for p be FinSequence of S st i in ( dom p) holds (p . i) in S

    proof

      let p be FinSequence of S;

      assume i in ( dom p);

      hence (p . i) in the carrier of S by FINSEQ_2: 11;

    end;

    theorem :: BSPACE:2

    (for i be Nat st i in ( dom p) holds (p . i) in S) implies p is FinSequence of S

    proof

      assume

       A1: for i be Nat st i in ( dom p) holds (p . i) in S;

      for i be Nat st i in ( dom p) holds (p . i) in the carrier of S by A1, STRUCT_0:def 5;

      hence thesis by FINSEQ_2: 12;

    end;

    scheme :: BSPACE:sch1

    IndSeqS { S() -> 1-sorted , P[ set] } :

for p be FinSequence of S() holds P[p]

      provided

       A1: P[( <*> S())]

       and

       A2: for p be FinSequence of S() holds for x be Element of S() st P[p] holds P[(p ^ <*x*>)];



       A3: P[( <*> the carrier of S())] by A1;

      thus for p be FinSequence of the carrier of S() holds P[p] from FINSEQ_2:sch 2( A3, A2);

    end;

    begin

    definition

      :: BSPACE:def2

      func Z_2 -> Field equals ( INT.Ring 2);

      coherence by INT_2: 28, INT_3: 12;

    end

    theorem :: BSPACE:3

    ( [#] Z_2 ) = { 0 , 1} by CARD_1: 50;

    theorem :: BSPACE:4

    for a be Element of Z_2 holds a = 0 or a = 1 by CARD_1: 50, TARSKI:def 2;

    theorem :: BSPACE:5



     Th5: ( 0. Z_2 ) = 0 by NAT_1: 44, SUBSET_1:def 8;

    theorem :: BSPACE:6



     Th6: ( 1. Z_2 ) = 1 by INT_3: 14;

    theorem :: BSPACE:7



     Th7: (( 1. Z_2 ) + ( 1. Z_2 )) = ( 0. Z_2 )

    proof

      (( 1. Z_2 ) + ( 1. Z_2 )) = ((1 + 1) mod 2) by Th6, GR_CY_1:def 4

      .= 0 by NAT_D: 25;

      hence thesis;

    end;

    theorem :: BSPACE:8

    for x be Element of Z_2 holds x = ( 0. Z_2 ) iff x <> ( 1. Z_2 ) by Th5, Th6, CARD_1: 50, TARSKI:def 2;

    begin

    definition

      let X be set, x be object;

      :: BSPACE:def3

      func X @ x -> Element of Z_2 equals

      : Def3: ( 1. Z_2 ) if x in X

      otherwise ( 0. Z_2 );

      coherence ;

      consistency ;

    end

    theorem :: BSPACE:9

    for X,x be set holds (X @ x) = ( 1. Z_2 ) iff x in X by Def3;

    theorem :: BSPACE:10

    for X,x be set holds (X @ x) = ( 0. Z_2 ) iff not x in X by Def3;

    theorem :: BSPACE:11

    for X,x be set holds (X @ x) <> ( 0. Z_2 ) iff (X @ x) = ( 1. Z_2 ) by Th5, Th6, CARD_1: 50, TARSKI:def 2;

    theorem :: BSPACE:12

    for X,x,y be set holds (X @ x) = (X @ y) iff (x in X iff y in X)

    proof

      let X,x,y be set;

      thus (X @ x) = (X @ y) implies (x in X iff y in X)

      proof

        assume

         A1: (X @ x) = (X @ y);

        thus x in X implies y in X

        proof

          assume x in X;

          then (X @ x) = ( 1. Z_2 ) by Def3;

          hence thesis by A1, Def3;

        end;

        assume y in X;

        then (X @ y) = ( 1. Z_2 ) by Def3;

        hence thesis by A1, Def3;

      end;

      assume

       A2: x in X iff y in X;

      per cases by Th5, Th6, CARD_1: 50, TARSKI:def 2;

        suppose (X @ x) = ( 0. Z_2 );

        hence thesis by A2, Def3;

      end;

        suppose (X @ x) = ( 1. Z_2 );

        hence thesis by A2, Def3;

      end;

    end;

    theorem :: BSPACE:13

    for X,Y,x be set holds (X @ x) = (Y @ x) iff (x in X iff x in Y)

    proof

      let X,Y,x be set;

      thus (X @ x) = (Y @ x) implies (x in X iff x in Y)

      proof

        assume

         A1: (X @ x) = (Y @ x);

        thus x in X implies x in Y

        proof

          assume x in X;

          then (X @ x) = ( 1. Z_2 ) by Def3;

          hence thesis by A1, Def3;

        end;

        assume x in Y;

        then (Y @ x) = ( 1. Z_2 ) by Def3;

        hence thesis by A1, Def3;

      end;

      thus (x in X iff x in Y) implies (X @ x) = (Y @ x)

      proof

        assume

         A2: x in X iff x in Y;

        per cases by Th5, Th6, CARD_1: 50, TARSKI:def 2;

          suppose (X @ x) = ( 0. Z_2 );

          hence thesis by A2, Def3;

        end;

          suppose (X @ x) = ( 1. Z_2 );

          hence thesis by A2, Def3;

        end;

      end;

    end;

    theorem :: BSPACE:14

    for x be set holds ( {} @ x) = ( 0. Z_2 ) by Def3;

    theorem :: BSPACE:15



     Th15: for X be set, u,v be Subset of X, x be Element of X holds ((u \+\ v) @ x) = ((u @ x) + (v @ x))

    proof

      let X be set, u,v be Subset of X, x be Element of X;

      per cases ;

        suppose

         A1: x in (u \+\ v);

        then

         A2: ((u \+\ v) @ x) = ( 1. Z_2 ) by Def3;

        per cases ;

          suppose

           A3: x in u;

          then not x in v by A1, XBOOLE_0: 1;

          then

           A4: (v @ x) = ( 0. Z_2 ) by Def3;

          (u @ x) = ( 1. Z_2 ) by A3, Def3;

          hence thesis by A2, A4, RLVECT_1: 4;

        end;

          suppose

           A5: not x in u;

          then x in v by A1, XBOOLE_0: 1;

          then

           A6: (v @ x) = ( 1. Z_2 ) by Def3;

          (u @ x) = ( 0. Z_2 ) by A5, Def3;

          hence thesis by A2, A6, RLVECT_1: 4;

        end;

      end;

        suppose

         A7: not x in (u \+\ v);

        then

         A8: ((u \+\ v) @ x) = ( 0. Z_2 ) by Def3;

        per cases ;

          suppose x in u;

          then x in v & (u @ x) = ( 1. Z_2 ) by A7, Def3, XBOOLE_0: 1;

          hence thesis by A8, Def3, Th7;

        end;

          suppose

           A9: not x in u;

          then not x in v by A7, XBOOLE_0: 1;

          then

           A10: (v @ x) = ( 0. Z_2 ) by Def3;

          (u @ x) = ( 0. Z_2 ) by A9, Def3;

          hence thesis by A8, A10, RLVECT_1: 4;

        end;

      end;

    end;

    theorem :: BSPACE:16

    for X,Y be set holds X = Y iff for x be object holds (X @ x) = (Y @ x)

    proof

      let X,Y be set;

      thus X = Y implies for x be object holds (X @ x) = (Y @ x);

      thus (for x be object holds (X @ x) = (Y @ x)) implies X = Y

      proof

        assume

         A1: for x be object holds (X @ x) = (Y @ x);

        thus X c= Y

        proof

          let y be object;

          assume y in X;

          then (X @ y) = ( 1. Z_2 ) by Def3;

          then (Y @ y) = ( 1. Z_2 ) by A1;

          hence thesis by Def3;

        end;

        let y be object;

        assume y in Y;

        then (Y @ y) = ( 1. Z_2 ) by Def3;

        then (X @ y) = ( 1. Z_2 ) by A1;

        hence thesis by Def3;

      end;

    end;

    begin

    definition

      let X be set, a be Element of Z_2 , c be Subset of X;

      :: BSPACE:def4

      func a \*\ c -> Subset of X equals

      : Def4: c if a = ( 1. Z_2 ),

( {} X) if a = ( 0. Z_2 );

      consistency ;

      coherence ;

    end

    definition

      let X be set;

      :: BSPACE:def5

      func bspace-sum (X) -> BinOp of ( bool X) means

      : Def5: for c,d be Subset of X holds (it . (c,d)) = (c \+\ d);

      existence

      proof

        defpred P[ set, set, set] means ex a,b be Subset of X st $1 = a & $2 = b & $3 = (a \+\ b);



         A1: for x,y be set st x in ( bool X) & y in ( bool X) holds ex z be set st z in ( bool X) & P[x, y, z]

        proof

          let x,y be set;

          assume x in ( bool X) & y in ( bool X);

          then

          reconsider x, y as Subset of X;

          set z = (x \+\ y);

          take z;

          thus thesis;

        end;

        consider f be Function of [:( bool X), ( bool X):], ( bool X) such that

         A2: for x,y be set st x in ( bool X) & y in ( bool X) holds P[x, y, (f . (x,y))] from BINOP_1:sch 9( A1);

        reconsider f as BinOp of ( bool X);

        take f;

        for c,d be Subset of X holds (f . (c,d)) = (c \+\ d)

        proof

          let c,d be Subset of X;

          ex a,b be Subset of X st c = a & d = b & (f . (c,d)) = (a \+\ b) by A2;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be BinOp of ( bool X) such that

         A3: (for c,d be Subset of X holds (f . (c,d)) = (c \+\ d)) & for c,d be Subset of X holds (g . (c,d)) = (c \+\ d);



         A4: for x be object st x in ( dom f) holds (f . x) = (g . x)

        proof

          let x be object;

          assume x in ( dom f);

          then

          consider y,z be object such that

           A5: y in ( bool X) and

           A6: z in ( bool X) and

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

          reconsider z as Subset of X by A6;

          reconsider y as Subset of X by A5;

          (f . (y,z)) = (y \+\ z) & (g . (y,z)) = (y \+\ z) by A3;

          hence thesis by A7;

        end;

        ( dom f) = [:( bool X), ( bool X):] by FUNCT_2:def 1;

        then ( dom f) = ( dom g) by FUNCT_2:def 1;

        hence thesis by A4;

      end;

    end

    theorem :: BSPACE:17



     Th17: for a be Element of Z_2 , c,d be Subset of X holds (a \*\ (c \+\ d)) = ((a \*\ c) \+\ (a \*\ d))

    proof

      let a be Element of Z_2 , c,d be Subset of X;

      per cases by Th5, Th6, CARD_1: 50, TARSKI:def 2;

        suppose

         A1: a = ( 0. Z_2 );

        then (a \*\ (c \+\ d)) = ( {} X) & (a \*\ c) = ( {} X) by Def4;

        hence thesis by A1, Def4;

      end;

        suppose

         A2: a = ( 1. Z_2 );

        then (a \*\ (c \+\ d)) = (c \+\ d) & (a \*\ c) = c by Def4;

        hence thesis by A2, Def4;

      end;

    end;

    theorem :: BSPACE:18



     Th18: for a,b be Element of Z_2 , c be Subset of X holds ((a + b) \*\ c) = ((a \*\ c) \+\ (b \*\ c))

    proof

      let a,b be Element of Z_2 , c be Subset of X;

      per cases by Th5, Th6, CARD_1: 50, TARSKI:def 2;

        suppose

         A1: a = ( 0. Z_2 );

        then (a \*\ c) = ( {} X) by Def4;

        hence thesis by A1, RLVECT_1: 4;

      end;

        suppose

         A2: a = ( 1. Z_2 );

        per cases by Th5, Th6, CARD_1: 50, TARSKI:def 2;

          suppose

           A3: b = ( 0. Z_2 );

          then (b \*\ c) = ( {} X) by Def4;

          hence thesis by A3, RLVECT_1: 4;

        end;

          suppose

           A4: b = ( 1. Z_2 );



           A5: (c \+\ c) = ( {} X) by XBOOLE_1: 92;

          (b \*\ c) = c by A4, Def4;

          hence thesis by A2, A4, A5, Def4, Th7;

        end;

      end;

    end;

    theorem :: BSPACE:19

    for c be Subset of X holds (( 1. Z_2 ) \*\ c) = c by Def4;

    theorem :: BSPACE:20



     Th20: for a,b be Element of Z_2 , c be Subset of X holds (a \*\ (b \*\ c)) = ((a * b) \*\ c)

    proof

      let a,b be Element of Z_2 , c be Subset of X;

      per cases by Th5, Th6, CARD_1: 50, TARSKI:def 2;

        suppose

         A1: a = ( 0. Z_2 );

        then (a \*\ (b \*\ c)) = ( {} X) by Def4;

        hence thesis by A1, Def4;

      end;

        suppose

         A2: a = ( 1. Z_2 );

        then (a \*\ (b \*\ c)) = (b \*\ c) by Def4;

        hence thesis by A2;

      end;

    end;

    definition

      let X be set;

      :: BSPACE:def6

      func bspace-scalar-mult (X) -> Function of [:the carrier of Z_2 , ( bool X):], ( bool X) means

      : Def6: for a be Element of Z_2 , c be Subset of X holds (it . (a,c)) = (a \*\ c);

      existence

      proof

        defpred P[ set, set, set] means ex a be Element of Z_2 , c be Subset of X st $1 = a & $2 = c & $3 = (a \*\ c);



         A1: for x,y be set st x in the carrier of Z_2 & y in ( bool X) holds ex z be set st z in ( bool X) & P[x, y, z]

        proof

          let x,y be set such that

           A2: x in the carrier of Z_2 and

           A3: y in ( bool X);

          reconsider y as Subset of X by A3;

          reconsider x as Element of Z_2 by A2;

          set z = (x \*\ y);

          take z;

          thus thesis;

        end;

        consider f be Function of [:the carrier of Z_2 , ( bool X):], ( bool X) such that

         A4: for x,y be set st x in the carrier of Z_2 & y in ( bool X) holds P[x, y, (f . (x,y))] from BINOP_1:sch 9( A1);

        take f;

        for a be Element of Z_2 , c be Subset of X holds (f . (a,c)) = (a \*\ c)

        proof

          let a be Element of Z_2 , c be Subset of X;

          ex a9 be Element of Z_2 , c9 be Subset of X st a = a9 & c = c9 & (f . (a,c)) = (a9 \*\ c9) by A4;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function of [:the carrier of Z_2 , ( bool X):], ( bool X) such that

         A5: (for a be Element of Z_2 , c be Subset of X holds (f . (a,c)) = (a \*\ c)) & for a be Element of Z_2 , c be Subset of X holds (g . (a,c)) = (a \*\ c);



         A6: for x be object st x in ( dom f) holds (f . x) = (g . x)

        proof

          let x be object;

          assume x in ( dom f);

          then

          consider y,z be object such that

           A7: y in the carrier of Z_2 and

           A8: z in ( bool X) and

           A9: x = [y, z] by ZFMISC_1:def 2;

          reconsider z as Subset of X by A8;

          reconsider y as Element of Z_2 by A7;

          (f . (y,z)) = (y \*\ z) & (g . (y,z)) = (y \*\ z) by A5;

          hence thesis by A9;

        end;

        ( dom f) = [:the carrier of Z_2 , ( bool X):] by FUNCT_2:def 1;

        then ( dom f) = ( dom g) by FUNCT_2:def 1;

        hence thesis by A6;

      end;

    end

    definition

      let X be set;

      :: BSPACE:def7

      func bspace (X) -> non empty ModuleStr over Z_2 equals ModuleStr (# ( bool X), ( bspace-sum X), ( {} X), ( bspace-scalar-mult X) #);

      coherence ;

    end



     Lm1: for a,b,c be Element of ( bspace X), A,B,C be Subset of X st a = A & b = B & c = C holds (a + (b + c)) = (A \+\ (B \+\ C)) & ((a + b) + c) = ((A \+\ B) \+\ C)

    proof

      let a,b,c be Element of ( bspace X);

      let A,B,C be Subset of X;

      assume that

       A1: a = A and

       A2: b = B and

       A3: c = C;

      (b + c) = (B \+\ C) by A2, A3, Def5;

      hence (a + (b + c)) = (A \+\ (B \+\ C)) by A1, Def5;

      (a + b) = (A \+\ B) by A1, A2, Def5;

      hence ((a + b) + c) = ((A \+\ B) \+\ C) by A3, Def5;

    end;



     Lm2: for a,b be Element of Z_2 , x,y be Element of ( bspace X), c,d be Subset of X st x = c & y = d holds ((a * x) + (b * y)) = ((a \*\ c) \+\ (b \*\ d)) & (a * (x + y)) = (a \*\ (c \+\ d)) & ((a + b) * x) = ((a + b) \*\ c) & ((a * b) * x) = ((a * b) \*\ c) & (a * (b * x)) = (a \*\ (b \*\ c))

    proof

      let a,b be Element of Z_2 , x,y be Element of ( bspace X), c,d be Subset of X such that

       A1: x = c and

       A2: y = d;

      (a * x) = (a \*\ c) & (b * y) = (b \*\ d) by A1, A2, Def6;

      hence ((a * x) + (b * y)) = ((a \*\ c) \+\ (b \*\ d)) by Def5;

      (x + y) = (c \+\ d) by A1, A2, Def5;

      hence (a * (x + y)) = (a \*\ (c \+\ d)) by Def6;

      thus ((a + b) * x) = ((a + b) \*\ c) by A1, Def6;

      thus ((a * b) * x) = ((a * b) \*\ c) by A1, Def6;

      (b * x) = (b \*\ c) by A1, Def6;

      hence (a * (b * x)) = (a \*\ (b \*\ c)) by Def6;

    end;

    theorem :: BSPACE:21



     Th21: ( bspace X) is Abelian

    proof

      let x,y be Element of ( bspace X);

      reconsider A = x, B = y as Subset of X;

      (x + y) = (B \+\ A) by Def5

      .= (y + x) by Def5;

      hence thesis;

    end;

    theorem :: BSPACE:22



     Th22: ( bspace X) is add-associative

    proof

      let x,y,z be Element of ( bspace X);

      reconsider A = x, B = y, C = z as Subset of X;

      (x + (y + z)) = (A \+\ (B \+\ C)) by Lm1

      .= ((A \+\ B) \+\ C) by XBOOLE_1: 91

      .= ((x + y) + z) by Lm1;

      hence thesis;

    end;

    theorem :: BSPACE:23



     Th23: ( bspace X) is right_zeroed

    proof

      let x be Element of ( bspace X);

      reconsider A = x as Subset of X;

      reconsider Z = ( 0. ( bspace X)) as Subset of X;

      (x + ( 0. ( bspace X))) = (A \+\ Z) by Def5

      .= x;

      hence thesis;

    end;

    theorem :: BSPACE:24



     Th24: ( bspace X) is right_complementable

    proof

      let x be Element of ( bspace X);

      reconsider A = x as Subset of X;

      take x;

      (A \+\ A) = ( {} X) by XBOOLE_1: 92;

      hence thesis by Def5;

    end;

    theorem :: BSPACE:25



     Th25: for a be Element of Z_2 , x,y be Element of ( bspace X) holds (a * (x + y)) = ((a * x) + (a * y))

    proof

      let a be Element of Z_2 , x,y be Element of ( bspace X);

      reconsider c = x, d = y as Subset of X;

      (a * (x + y)) = (a \*\ (c \+\ d)) by Lm2

      .= ((a \*\ c) \+\ (a \*\ d)) by Th17

      .= ((a * x) + (a * y)) by Lm2;

      hence thesis;

    end;

    theorem :: BSPACE:26



     Th26: for a,b be Element of Z_2 , x be Element of ( bspace X) holds ((a + b) * x) = ((a * x) + (b * x))

    proof

      let a,b be Element of Z_2 , x be Element of ( bspace X);

      reconsider c = x as Subset of X;

      ((a + b) * x) = ((a + b) \*\ c) by Lm2

      .= ((a \*\ c) \+\ (b \*\ c)) by Th18

      .= ((a * x) + (b * x)) by Lm2;

      hence thesis;

    end;

    theorem :: BSPACE:27



     Th27: for a,b be Element of Z_2 , x be Element of ( bspace X) holds ((a * b) * x) = (a * (b * x))

    proof

      let a,b be Element of Z_2 , x be Element of ( bspace X);

      reconsider c = x as Subset of X;

      ((a * b) * x) = ((a * b) \*\ c) by Lm2

      .= (a \*\ (b \*\ c)) by Th20

      .= (a * (b * x)) by Lm2;

      hence thesis;

    end;

    theorem :: BSPACE:28



     Th28: for x be Element of ( bspace X) holds (( 1_ Z_2 ) * x) = x

    proof

      let x be Element of ( bspace X);

      reconsider c = x as Subset of X;

      (( 1_ Z_2 ) * x) = (( 1_ Z_2 ) \*\ c) by Def6

      .= c by Def4;

      hence thesis;

    end;

    theorem :: BSPACE:29



     Th29: ( bspace X) is vector-distributive scalar-distributive scalar-associative scalar-unital by Th25, Th26, Th27, Th28;

    registration

      let X be set;

      cluster ( bspace X) -> vector-distributive scalar-distributive scalar-associative scalar-unital Abelian right_complementable add-associative right_zeroed;

      coherence by Th21, Th22, Th23, Th24, Th29;

    end

    begin

    definition

      let X be set;

      :: BSPACE:def8

      func singletons (X) -> set equals { f where f be Subset of X : f is 1 -element };

      coherence ;

    end

    definition

      let X be set;

      :: original: singletons

      redefine

      func singletons (X) -> Subset of ( bspace X) ;

      coherence

      proof

        set S = ( singletons X);

        S c= ( bool X)

        proof

          let f be object;

          assume f in S;

          then ex g be Subset of X st f = g & g is 1 -element;

          then

          reconsider f as Subset of X;

          f is Element of ( bool X);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let X be non empty set;

      cluster ( singletons X) -> non empty;

      coherence

      proof

        set x = the Element of X;

         {x} in ( singletons X);

        hence thesis;

      end;

    end

    theorem :: BSPACE:30



     Th30: for X be non empty set, f be Subset of X st f is Element of ( singletons X) holds f is 1 -element

    proof

      let X be non empty set, f be Subset of X;

      assume f is Element of ( singletons X);

      then f in ( singletons X);

      then ex g be Subset of X st g = f & g is 1 -element;

      hence thesis;

    end;

    definition

      let F be Field, V be VectSp of F, l be Linear_Combination of V, x be Element of V;

      :: original: .

      redefine

      func l . x -> Element of F ;

      coherence

      proof

        (l . x) in ( [#] F);

        hence thesis;

      end;

    end

    definition

      let X be non empty set, s be FinSequence of ( bspace X), x be Element of X;

      :: BSPACE:def9

      func s @ x -> FinSequence of Z_2 means

      : Def9: ( len it ) = ( len s) & for j be Nat st 1 <= j & j <= ( len s) holds (it . j) = ((s . j) @ x);

      existence

      proof

        deffunc F( set) = ((s . $1) @ x);

        consider p be FinSequence such that

         A1: ( len p) = ( len s) and

         A2: for k be Nat st k in ( dom p) holds (p . k) = F(k) from FINSEQ_1:sch 2;



         A3: for j be Nat st 1 <= j & j <= ( len s) holds (p . j) = ((s . j) @ x) by A1, FINSEQ_3: 25, A2;

        ( rng p) c= the carrier of Z_2

        proof

          let y be object;

          assume y in ( rng p);

          then

          consider a be object such that

           A4: a in ( dom p) and

           A5: (p . a) = y by FUNCT_1:def 3;

          (p . a) = ((s . a) @ x) by A2, A4;

          hence thesis by A5;

        end;

        then

        reconsider p as FinSequence of Z_2 by FINSEQ_1:def 4;

        take p;

        thus thesis by A1, A3;

      end;

      uniqueness

      proof

        let f,g be FinSequence of Z_2 such that

         A6: ( len f) = ( len s) and

         A7: for j be Nat st 1 <= j & j <= ( len s) holds (f . j) = ((s . j) @ x) and

         A8: ( len g) = ( len s) and

         A9: for j be Nat st 1 <= j & j <= ( len s) holds (g . j) = ((s . j) @ x);

        for k be Nat st 1 <= k & k <= ( len f) holds (f . k) = (g . k)

        proof

          let k be Nat such that

           A10: 1 <= k & k <= ( len f);

          (f . k) = ((s . k) @ x) by A6, A7, A10;

          hence thesis by A6, A9, A10;

        end;

        hence thesis by A6, A8;

      end;

    end

    theorem :: BSPACE:31



     Th31: for X be non empty set, x be Element of X holds (( <*> ( bspace X)) @ x) = ( <*> Z_2 )

    proof

      let X be non empty set, x be Element of X;

      set V = ( bspace X);

      set L = (( <*> V) @ x);

      ( len L) = ( len ( <*> V)) by Def9

      .= 0 ;

      hence thesis;

    end;

    theorem :: BSPACE:32



     Th32: for X be set, u,v be Element of ( bspace X), x be Element of X holds ((u + v) @ x) = ((u @ x) + (v @ x))

    proof

      let X be set, u,v be Element of ( bspace X), x be Element of X;

      reconsider u9 = u, v9 = v as Subset of X;

      ((u + v) @ x) = ((u9 \+\ v9) @ x) by Def5

      .= ((u9 @ x) + (v9 @ x)) by Th15;

      hence thesis;

    end;

    theorem :: BSPACE:33



     Th33: for X be non empty set, s be FinSequence of ( bspace X), f be Element of ( bspace X), x be Element of X holds ((s ^ <*f*>) @ x) = ((s @ x) ^ <*(f @ x)*>)

    proof

      let X be non empty set, s be FinSequence of ( bspace X), f be Element of ( bspace X), x be Element of X;

      set L = ((s ^ <*f*>) @ x);

      set R = ((s @ x) ^ <*(f @ x)*>);



       A1: ( len L) = ( len (s ^ <*f*>)) by Def9

      .= (( len s) + ( len <*f*>)) by FINSEQ_1: 22

      .= (( len s) + 1) by FINSEQ_1: 39;



       A2: for k be Nat st 1 <= k & k <= ( len L) holds (L . k) = (R . k)

      proof

        let k be Nat such that

         A3: 1 <= k and

         A4: k <= ( len L);

        per cases by A1, A4, NAT_1: 8;

          suppose

           A5: k <= ( len s);

          ( dom (s @ x)) = ( Seg ( len (s @ x))) by FINSEQ_1:def 3

          .= ( Seg ( len s)) by Def9;

          then k in ( dom (s @ x)) by A3, A5;



          then

           A6: (R . k) = ((s @ x) . k) by FINSEQ_1:def 7

          .= ((s . k) @ x) by A3, A5, Def9;

          ( dom s) = ( Seg ( len s)) by FINSEQ_1:def 3;

          then

           A7: k in ( dom s) by A3, A5;

          k <= ( len (s ^ <*f*>)) by A4, Def9;

          then (L . k) = (((s ^ <*f*>) . k) @ x) by A3, Def9;

          hence thesis by A6, A7, FINSEQ_1:def 7;

        end;

          suppose

           A8: k = ( len L);

          ( dom <*(f @ x)*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

          then

           A9: 1 in ( dom <*(f @ x)*>) by TARSKI:def 1;

          ( len (s @ x)) = ( len s) by Def9;



          then

           A10: (R . k) = ( <*(f @ x)*> . 1) by A1, A8, A9, FINSEQ_1:def 7

          .= (f @ x) by FINSEQ_1:def 8;

          ( dom <*f*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

          then 1 in ( dom <*f*>) by TARSKI:def 1;



          then

           A11: ((s ^ <*f*>) . k) = ( <*f*> . 1) by A1, A8, FINSEQ_1:def 7

          .= f by FINSEQ_1:def 8;

          k <= ( len (s ^ <*f*>)) by A4, Def9;

          hence thesis by A3, A10, A11, Def9;

        end;

      end;

      ( len ((s @ x) ^ <*(f @ x)*>)) = (( len (s @ x)) + ( len <*(f @ x)*>)) by FINSEQ_1: 22

      .= (( len s) + ( len <*(f @ x)*>)) by Def9

      .= (( len s) + 1) by FINSEQ_1: 39;

      hence thesis by A1, A2;

    end;

    theorem :: BSPACE:34



     Th34: for X be non empty set, s be FinSequence of ( bspace X), x be Element of X holds (( Sum s) @ x) = ( Sum (s @ x))

    proof

      let X be non empty set, s be FinSequence of ( bspace X), x be Element of X;

      set V = ( bspace X);

      defpred Q[ FinSequence of V] means (( Sum $1) @ x) = ( Sum ($1 @ x));



       A1: Q[( <*> V)]

      proof

        reconsider z = ( 0. V) as Subset of X;

        set e = ( <*> V);



         A2: (z @ x) = ( 0. Z_2 ) by Def3;

        ( Sum e) = ( 0. V) & (e @ x) = ( <*> Z_2 ) by Th31, RLVECT_1: 43;

        hence thesis by A2, RLVECT_1: 43;

      end;



       A3: for p be FinSequence of V, f be Element of V st Q[p] holds Q[(p ^ <*f*>)]

      proof

        let p be FinSequence of V, f be Element of V such that

         A4: Q[p];

        (( Sum (p ^ <*f*>)) @ x) = ((( Sum p) + ( Sum <*f*>)) @ x) by RLVECT_1: 41

        .= ((( Sum p) + f) @ x) by RLVECT_1: 44

        .= ((( Sum p) @ x) + (f @ x)) by Th32

        .= (( Sum (p @ x)) + ( Sum <*(f @ x)*>)) by A4, RLVECT_1: 44

        .= ( Sum ((p @ x) ^ <*(f @ x)*>)) by RLVECT_1: 41

        .= ( Sum ((p ^ <*f*>) @ x)) by Th33;

        hence thesis;

      end;

      for p be FinSequence of V holds Q[p] from IndSeqS( A1, A3);

      hence thesis;

    end;

    theorem :: BSPACE:35



     Th35: for X be non empty set, l be Linear_Combination of ( bspace X), x be Element of ( bspace X) st x in ( Carrier l) holds (l . x) = ( 1_ Z_2 )

    proof

      let X be non empty set, l be Linear_Combination of ( bspace X), x be Element of ( bspace X);

      assume x in ( Carrier l);

      then (l . x) <> ( 0. Z_2 ) by VECTSP_6: 2;

      hence thesis by Th5, Th6, CARD_1: 50, TARSKI:def 2;

    end;

    registration

      let X be empty set;

      cluster ( singletons X) -> empty;

      coherence

      proof

        assume ( singletons X) is non empty;

        then

        consider f be object such that

         A1: f in ( singletons X);

        ex g be Subset of X st g = f & g is 1 -element by A1;

        hence thesis;

      end;

    end

    theorem :: BSPACE:36



     Th36: ( singletons X) is linearly-independent

    proof

      per cases ;

        suppose X is empty;

        hence thesis;

      end;

        suppose X is non empty;

        then

        reconsider X as non empty set;

        set V = ( bspace X);

        set S = ( singletons X);

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

        proof

          let l be Linear_Combination of S such that

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

          reconsider s = ( Sum l) as Subset of X;

          set C = ( Carrier l);



           A2: (l ! ( Carrier l)) = l by RANKNULL: 24;

          assume C <> {} ;

          then

          consider f be Element of V such that

           A3: f in C by SUBSET_1: 4;

          reconsider f as Subset of X;

          reconsider g = f as Element of V;



           A4: {g} c= ( Carrier l) by A3, ZFMISC_1: 31;

          reconsider n = (l ! {g}) as Linear_Combination of {g};

          reconsider m = (l ! (C \ {g})) as Linear_Combination of (C \ {g});

          reconsider l as Linear_Combination of C by A2;

          reconsider t = ( Sum m), u = ( Sum n) as Subset of X;

          g in {g} by TARSKI:def 1;

          then

           A5: ( Sum n) = ((n . g) * g) & (n . g) = (l . g) by RANKNULL: 25, VECTSP_6: 17;

          (l . g) <> ( 0. Z_2 ) by A3, VECTSP_6: 2;

          then (l . g) = ( 1_ Z_2 ) by Th5, Th6, CARD_1: 50, TARSKI:def 2;

          then

           A6: u = f by A5, VECTSP_1:def 17;

          C c= S by VECTSP_6:def 4;

          then f is 1 -element by A3, Th30;

          then

          consider x be Element of X such that

           A7: f = {x} by CARD_1: 65;

          x in f by A7, TARSKI:def 1;

          then

           A8: (f @ x) = ( 1. Z_2 ) by Def3;



           A9: for g be Subset of X st g <> f & g in C holds (g @ x) = ( 0. Z_2 )

          proof

            let g be Subset of X such that

             A10: g <> f and

             A11: g in C;

            C c= S by VECTSP_6:def 4;

            then g is 1 -element by A11, Th30;

            then

            consider y be Element of X such that

             A12: g = {y} by CARD_1: 65;

            now

              assume (g @ x) <> ( 0. Z_2 );

              then x in {y} by A12, Def3;

              hence contradiction by A7, A10, A12, TARSKI:def 1;

            end;

            hence thesis;

          end;



           A13: (t @ x) = 0

          proof

            consider F be FinSequence of V such that

             A14: F is one-to-one & ( rng F) = ( Carrier m) and

             A15: t = ( Sum (m (#) F)) by VECTSP_6:def 6;



             A16: (( Sum (m (#) F)) @ x) = ( Sum ((m (#) F) @ x)) by Th34;

            for F be FinSequence of V st F is one-to-one & ( rng F) = ( Carrier m) holds ((m (#) F) @ x) = (( len F) |-> ( 0. Z_2 ))

            proof

              let F be FinSequence of V such that F is one-to-one and

               A17: ( rng F) = ( Carrier m);

              set R = (( len F) |-> ( 0. Z_2 ));

              set L = ((m (#) F) @ x);



               A18: ( len (m (#) F)) = ( len F) by VECTSP_6:def 5;

              then

               A19: ( len L) = ( len F) by Def9;



               A20: for k be Nat st 1 <= k & k <= ( len L) holds (L . k) = (R . k)

              proof

                let k be Nat such that

                 A21: 1 <= k & k <= ( len L);



                 A22: k in ( Seg ( len F)) by A19, A21;

                ( len (m (#) F)) = ( len F) by VECTSP_6:def 5;

                then ( dom (m (#) F)) = ( Seg ( len F)) by FINSEQ_1:def 3;

                then k in ( dom (m (#) F)) by A19, A21;

                then

                 A23: ((m (#) F) . k) = ((m . (F /. k)) * (F /. k)) by VECTSP_6:def 5;

                reconsider Fk = (F /. k) as Subset of X;



                 A24: ( Carrier m) c= (C \ {f}) by VECTSP_6:def 4;

                ( dom F) = ( Seg ( len F)) by FINSEQ_1:def 3;

                then

                 A25: k in ( dom F) by A19, A21;

                then

                 A26: (F /. k) = (F . k) by PARTFUN1:def 6;

                then (m . (F /. k)) = ( 1_ Z_2 ) by A17, A25, Th35, FUNCT_1: 3;

                then

                 A27: ((m (#) F) . k) = Fk by A23, VECTSP_1:def 17;



                 A28: (F /. k) in ( Carrier m) by A17, A25, A26, FUNCT_1: 3;

                then

                 A29: Fk in C by A24, XBOOLE_0:def 5;



                 A30: Fk <> f

                proof

                  assume Fk = f;

                  then not f in {f} by A28, A24, XBOOLE_0:def 5;

                  hence contradiction by TARSKI:def 1;

                end;

                (L . k) = (((m (#) F) . k) @ x) by A18, A19, A21, Def9

                .= ( 0. Z_2 ) by A9, A27, A30, A29;

                hence thesis by A22, FUNCOP_1: 7;

              end;

              ( dom R) = ( Seg ( len F)) by FUNCOP_1: 13;

              then ( len L) = ( len R) by A19, FINSEQ_1:def 3;

              hence thesis by A20;

            end;

            then ((m (#) F) @ x) = (( len F) |-> ( 0. Z_2 )) by A14;

            hence thesis by A15, A16, Th5, MATRIX_3: 11;

          end;

          l = (n + m) by A4, RANKNULL: 27;

          then ( Sum l) = (( Sum m) + ( Sum n)) by VECTSP_6: 44;

          then s = (t \+\ u) by Def5;

          then

           A31: (s @ x) = ((t @ x) + (u @ x)) by Th15;

          (s @ x) = ( 0. Z_2 ) by A1, Def3;

          hence thesis by A8, A31, A13, A6, RLVECT_1: 4;

        end;

        hence thesis by VECTSP_7:def 1;

      end;

    end;

    theorem :: BSPACE:37

    for f be Element of ( bspace X) st (ex x be set st x in X & f = {x}) holds f in ( singletons X);

    theorem :: BSPACE:38



     Th38: for X be finite set, A be Subset of X holds ex l be Linear_Combination of ( singletons X) st ( Sum l) = A

    proof

      let X be finite set, A be Subset of X;

      set V = ( bspace X);

      set S = ( singletons X);

      defpred P[ set] means $1 is Subset of X implies ex l be Linear_Combination of S st ( Sum l) = $1;



       A1: P[ {} ]

      proof

        reconsider l = ( ZeroLC V) as Linear_Combination of S by VECTSP_6: 5;

        assume {} is Subset of X;

        take l;

        ( Sum l) = ( 0. V) by VECTSP_6: 15;

        hence thesis;

      end;



       A2: for x,B be set st x in A & B c= A & P[B] holds P[(B \/ {x})]

      proof

        let x,B be set such that x in A and B c= A and

         A3: P[B];

        assume

         A4: (B \/ {x}) is Subset of X;

        then

        reconsider B as Subset of X by XBOOLE_1: 11;

        consider l be Linear_Combination of S such that

         A5: ( Sum l) = B by A3;

        per cases ;

          suppose

           A6: x in B;

          take l;

          thus thesis by A5, A6, ZFMISC_1: 40;

        end;

          suppose not x in B;

          then

           A7: B misses {x} by ZFMISC_1: 50;

          reconsider z = ( ZeroLC V) as Linear_Combination of ( {} V) by VECTSP_6: 5;

          reconsider f = {x} as Element of V by A4, XBOOLE_1: 11;

          reconsider g = f as Subset of X;

          set m = (z +* (f,( 1_ Z_2 )));

          m is Linear_Combination of (( {} V) \/ {f}) by RANKNULL: 23;

          then

          reconsider m = (z +* (f,( 1_ Z_2 ))) as Linear_Combination of {f};

          ( dom z) = ( [#] V) by FUNCT_2: 92;

          then

           A8: (m . f) = ( 1_ Z_2 ) by FUNCT_7: 31;

          f in S;

          then {f} c= S by ZFMISC_1: 31;

          then m is Linear_Combination of S by VECTSP_6: 4;

          then

          reconsider n = (l + m) as Linear_Combination of S by VECTSP_6: 24;

          take n;

          ( Sum n) = (( Sum l) + ( Sum m)) by VECTSP_6: 44

          .= (( Sum l) + ((m . f) * f)) by VECTSP_6: 17

          .= (( Sum l) + f) by A8, VECTSP_1:def 17

          .= (B \+\ g) by A5, Def5

          .= ((B \/ {x}) \ (B /\ {x})) by XBOOLE_1: 101

          .= ((B \/ {x}) \ {} ) by A7

          .= (B \/ {x});

          hence thesis;

        end;

      end;



       A9: A is finite;

       P[A] from FINSET_1:sch 2( A9, A1, A2);

      hence thesis;

    end;

    theorem :: BSPACE:39



     Th39: for X be finite set holds ( Lin ( singletons X)) = ( bspace X)

    proof

      let X be finite set;

      set V = ( bspace X);

      set S = ( singletons X);

      for v be Element of V holds v in ( Lin S)

      proof

        let v be Element of V;

        reconsider f = v as Subset of X;

        consider A be set such that

         A1: A c= X and

         A2: f = A;

        reconsider A as Subset of X by A1;

        ex l be Linear_Combination of S st ( Sum l) = A by Th38;

        hence thesis by A2, VECTSP_7: 7;

      end;

      hence thesis by VECTSP_4: 32;

    end;

    theorem :: BSPACE:40



     Th40: for X be finite set holds ( singletons X) is Basis of ( bspace X)

    proof

      let X be finite set;

      ( singletons X) is linearly-independent & ( Lin ( singletons X)) = ( bspace X) by Th36, Th39;

      hence thesis by VECTSP_7:def 3;

    end;

    registration

      let X be finite set;

      cluster ( singletons X) -> finite;

      coherence ;

    end

    registration

      let X be finite set;

      cluster ( bspace X) -> finite-dimensional;

      coherence

      proof

        set S = ( singletons X);

        S is Basis of ( bspace X) by Th40;

        hence thesis by MATRLIN:def 1;

      end;

    end

    theorem :: BSPACE:41

    ( card ( singletons X)) = ( card X)

    proof

      defpred P[ object, object] means $1 in X & $2 = {$1};



       A1: for x be object st x in X holds ex y be object st P[x, y];

      consider f be Function such that

       A2: ( dom f) = X and

       A3: for x be object st x in X holds P[x, (f . x)] from CLASSES1:sch 1( A1);



       A4: ( rng f) = ( singletons X)

      proof

        thus ( rng f) c= ( singletons X)

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A5: x in ( dom f) and

           A6: y = (f . x) by FUNCT_1:def 3;



           A7: (f . x) = {x} by A2, A3, A5;

          then

          reconsider fx = (f . x) as Subset of X by A2, A5, ZFMISC_1: 31;

          fx is 1 -element by A7;

          hence thesis by A6;

        end;

        let y be object such that

         A8: y in ( singletons X);

        reconsider X as non empty set by A8;

        ex z be Subset of X st y = z & z is 1 -element by A8;

        then

        reconsider y as 1 -element Subset of X;

        consider x be Element of X such that

         A9: y = {x} by CARD_1: 65;

        y = (f . x) by A3, A9;

        hence thesis by A2, FUNCT_1: 3;

      end;

      f is one-to-one

      proof

        let x1,x2 be object such that

         A10: x1 in ( dom f) & x2 in ( dom f) and

         A11: (f . x1) = (f . x2);

         P[x1, (f . x1)] & P[x2, (f . x2)] by A2, A3, A10;

        hence thesis by A11, ZFMISC_1: 3;

      end;

      then (X,( singletons X)) are_equipotent by A2, A4, WELLORD2:def 4;

      hence thesis by CARD_1: 5;

    end;

    theorem :: BSPACE:42

    ( card ( [#] ( bspace X))) = ( exp (2,( card X))) by CARD_2: 31;

    theorem :: BSPACE:43

    ( dim ( bspace {} )) = 0

    proof

      ( card ( [#] ( bspace {} ))) = 1 by CARD_2: 42, ZFMISC_1: 1;

      hence thesis by RANKNULL: 5;

    end;