:: The Vector Space of Subsets of a Set Based on Symmetric Difference
::  by Jesse Alama
::
:: Received October 9, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, STRUCT_0, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, NAT_1,
      ORDINAL4, VECTSP_1, INT_3, CARD_1, SUPINF_2, MESFUNC1, ARYTM_3, INT_1,
      QC_LANG1, XBOOLE_0, TARSKI, BINOP_1, ZFMISC_1, RLVECT_1, ALGSTR_0,
      GROUP_1, RLVECT_2, XXREAL_0, CARD_3, RLVECT_3, REALSET1, VALUED_1,
      FINSEQ_2, PARTFUN1, FINSET_1, FUNCT_4, RLVECT_5, ORDINAL2, BSPACE;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, DOMAIN_1, RELSET_1,
      FUNCT_1, NUMBERS, ORDINAL1, NAT_1, INT_1, PARTFUN1, FUNCT_2, BINOP_1,
      FUNCT_7, XXREAL_0, CARD_1, FINSET_1, FINSEQ_1, FINSEQ_2,
      FINSEQOP, CARD_2,
      STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, VECTSP_6, VECTSP_7,
      MATRLIN, VECTSP_9, INT_3, RANKNULL;
 constructors FINSEQOP, VECTSP_7, VECTSP_9, REALSET1, WELLORD2, NAT_D, FUNCT_7,
      CARD_2, RANKNULL, INT_3, GR_CY_1, RELSET_1, BINOP_2, BINOP_1;
 registrations STRUCT_0, CARD_1, FINSET_1, FINSEQ_1, SUBSET_1, XBOOLE_0,
      VECTSP_1, ORDINAL1, XREAL_0, INT_1, VECTSP_7, RELSET_1;
 requirements NUMERALS, BOOLE, ARITHM, SUBSET, REAL;
 definitions TARSKI, FUNCT_1, FINSEQ_1, CARD_1, XBOOLE_0, VECTSP_1, RLVECT_1,
      STRUCT_0, FINSEQ_2, BINOP_1, INT_3, ALGSTR_0;
 theorems TARSKI, ZFMISC_1, FINSEQ_1, FUNCT_1, VECTSP_7, CARD_2, XBOOLE_1,
      FUNCT_2, SUBSET_1, XBOOLE_0, VECTSP_1, RLVECT_1, VECTSP_4, VECTSP_6,
      STRUCT_0, CARD_1, FUNCOP_1, FUNCT_7, FINSEQ_2, NAT_1, WELLORD2, RANKNULL,
      MATRIX_3, INT_2, INT_3, GR_CY_1, NAT_D, ORDINAL1, PARTFUN1, FINSEQ_3,
      MATRLIN;
 schemes FINSEQ_1, FINSET_1, BINOP_1, FINSEQ_2, CLASSES1;

begin

definition
  let S be 1-sorted;
  func <*>S -> FinSequence of S equals
  <*>([#]S);
  coherence;
end;

:: exactly as in FINSEQ_2

reserve S for 1-sorted,
  i for Element of NAT,
  p for FinSequence,
  X for set;

:: copied from FINSEQ_2:13

theorem
  for p being 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;

:: copied from FINSEQ_2:14

theorem
  (for i being Nat st i in dom p holds p.i in S) implies p is FinSequence of S
proof
  assume
A1: for i being Nat st i in dom p holds p.i in S;
  for i being Nat st i in dom p holds p.i in the carrier of S
  proof
    let i be Nat;
    assume i in dom p;
    then p.i in S by A1;
    hence thesis by STRUCT_0:def 5;
  end;
  hence thesis by FINSEQ_2:12;
end;

scheme
  IndSeqS{S() -> 1-sorted, P[set]}: for p being FinSequence of S() holds P[p]
provided
A1: P[<*> S()] and
A2: for p being FinSequence of S() for x being Element of S() st P[p]
holds P[p^<*x*>]
proof
A3: P[<*>the carrier of S()] by A1;
  thus for p being FinSequence of the carrier of S() holds P[p] from FINSEQ_2:
  sch 2(A3,A2);
end;

begin :: The two-element field Z_2

definition
  func Z_2 -> Field equals
  INT.Ring(2);
  coherence by INT_2:28,INT_3:12;
end;

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

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

theorem Th5:
  0.Z_2 = 0
proof
 0 in 2 by NAT_1:44;
 hence 0.Z_2 = 0 by FUNCT_7:def 1;
end;

theorem Th6:
  1.Z_2 = 1 by INT_3:14;

theorem 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 by FUNCT_7:def 1;
end;

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

begin :: Set-theoretical Preliminaries

definition
  let X,x be set;
  func X@x -> Element of Z_2 equals
  :Def3:
  1.Z_2 if x in X otherwise 0.Z_2;
  coherence;
  consistency;
end;

theorem
  for X,x being set holds X@x = 1.Z_2 iff x in X by Def3;

theorem
  for X,x being set holds X@x = 0.Z_2 iff not x in X by Def3;

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

theorem
  for X,x,y being 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
  for X,Y,x being 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
  for x being set holds {}@x = 0.Z_2 by Def3;

theorem Th15:
  for X being set, u,v being Subset of X, x being 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
  for X,Y being set holds X = Y iff for x being set holds X@x = Y@x
proof
  let X,Y be set;
  thus X = Y implies for x being set holds X@x = Y@x;
  thus (for x being set holds X@x = Y@x) implies X = Y
  proof
    assume
A1: for x being set holds X@x = Y@x;
    thus X c= Y
    proof
      let y be set;
      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 set;
    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 :: The Boolean Bector Space of Subsets of a Set

definition
  let X be set, a be Element of Z_2, c be Subset of X;
  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;
  func bspace-sum(X) -> BinOp of bool X means
  :Def5:
  for c,d being Subset of X holds it.(c,d) = c \+\ d;
  existence
  proof
    defpred P[set,set,set] means ex a,b being Subset of X st $1 = a & $2 = b &
    $3 = a \+\ b;
A1: for x,y being set st x in bool X & y in bool X ex z being 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 being Function of [:bool X,bool X:],bool X such that
A2: for x,y being set st x in bool X & y in bool X holds P[x,y,f.(x,y)
    ] from BINOP_1:sch 1(A1);
    reconsider f as BinOp of bool X;
    take f;
    for c,d being Subset of X holds f.(c,d) = c \+\ d
    proof
      let c,d be Subset of X;
      ex a,b being 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 being Subset of X holds f.(c,d) = c \+\ d)& for c,d
    being Subset of X holds g.(c,d) = c \+\ d;
A4: for x being set st x in dom f holds f.x = g.x
    proof
      let x be set;
      assume x in dom f;
      then consider y,z being set 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,FUNCT_1:2;
  end;
end;

theorem Th17:
  for a being Element of Z_2, c,d being 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 Th18:
  for a,b being Element of Z_2, c being 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
  for c being Subset of X holds (1.Z_2) \*\ c = c by Def4;

theorem Th20:
  for a,b being Element of Z_2, c being 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,VECTSP_1:7;
  end;
  suppose
A2: a = 1.Z_2;
    then a \*\ (b \*\ c) = b \*\ c by Def4;
    hence thesis by A2,VECTSP_1:def 6;
  end;
end;

definition
  let X be set;
  func bspace-scalar-mult(X) -> Function of [:the carrier of Z_2,bool X:],bool
  X means
  :Def6:
  for a being Element of Z_2, c being Subset of X holds it.(a,c) = a \*\ c;
  existence
  proof
    defpred P[set,set,set] means ex a being Element of Z_2, c being Subset of
    X st $1 = a & $2 = c & $3 = a \*\ c;
A1: for x,y being set st x in the carrier of Z_2 & y in bool X ex z being
    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 being Function of [:the carrier of Z_2,bool X:],bool X such
    that
A4: for x,y being set st x in the carrier of Z_2 & y in bool X holds P
    [x,y,f.(x,y)] from BINOP_1:sch 1(A1);
    take f;
    for a being Element of Z_2, c being Subset of X holds f.(a,c) = a \*\ c
    proof
      let a be Element of Z_2, c be Subset of X;
      ex a9 being Element of Z_2, c9 being 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 being Element of Z_2, c being Subset of X holds f.(a,c) =
a \*\ c)& for a being Element of Z_2, c being Subset of X holds g.(a,c) = a \*\
    c;
A6: for x being set st x in dom f holds f.x = g.x
    proof
      let x be set;
      assume x in dom f;
      then consider y,z being set 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,FUNCT_1:2;
  end;
end;

definition
  let X be set;
  func bspace(X) -> non empty VectSpStr over Z_2 equals
  VectSpStr (# bool X,
    bspace-sum(X), {}X, bspace-scalar-mult(X) #);
  coherence;
end;

Lm1: for a,b,c being Element of bspace(X), A,B,C being 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 being Element of Z_2, x,y being Element of bspace(X), c,d being
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 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 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 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 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 Th25:
  for a being Element of Z_2, x,y being 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 Th26:
  for a,b being Element of Z_2, x being 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 Th27:
  for a,b being Element of Z_2, x being 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 Th28:
  for x being 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 Th29:
  bspace(X) is vector-distributive scalar-distributive
  scalar-associative scalar-unital
proof
 thus bspace X is vector-distributive
  proof
   let a be Element of Z_2, x,y be Element of bspace(X);
   thus a*(x+y) = (a*x)+(a*y) by Th25;
  end;
 thus bspace X is scalar-distributive
  proof
  let a,b be Element of Z_2, x be Element of bspace(X);
   thus (a+b)*x = (a*x)+(b*x) by Th26;
  end;
 thus bspace X is scalar-associative
  proof
  let a,b be Element of Z_2, x be Element of bspace(X);
  thus (a*b)*x = a*(b*x) by Th27;
  end;
  let x be Element of bspace(X);
  thus (1.Z_2)*x = x by Th28;
end;

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 :: The Linear Independence and Linear Span of 1-element Subsets

definition

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

definition
  let X be set;
  redefine func singletons(X) -> Subset of bspace(X);
  coherence
  proof
    set S = singletons(X);
    S c= bool(X)
    proof
      let f be set;
      assume f in S;
      then ex g being 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 Th30:
  for X being non empty set, f being 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 being 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;
  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;
  func s@x -> FinSequence of Z_2 means
  :Def9:
  len it = len s & for j being Nat st 1 <= j & j <= len s holds it.j = (s.j)@x;
  existence
  proof
    deffunc F(set) = (s.$1)@x;
    consider p being FinSequence such that
A1: len p = len s and
A2: for k being Nat st k in dom p holds p.k = F(k) from FINSEQ_1:sch 2;
A3: for j being Nat st 1 <= j & j <= len s holds p.j = (s.j)@x
    proof
      let j be Nat;
      assume 1 <= j & j <= len s;
      then j in dom p by A1,FINSEQ_3:25;
      hence thesis by A2;
    end;
    rng p c= the carrier of Z_2
    proof
      let y be set;
      assume y in rng p;
      then consider a being set 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 being Nat st 1 <= j & j <= len s holds f.j = (s.j)@x and
A8: len g = len s and
A9: for j being Nat st 1 <= j & j <= len s holds g.j = (s.j)@x;
    for k being 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,FINSEQ_1:14;
  end;
end;

theorem Th31:
  for X being non empty set, x being 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 Th32:
  for X being set, u,v being Element of bspace(X), x being 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 Th33:
  for X being non empty set, s being FinSequence of bspace(X), f
being Element of bspace(X), x being 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 being 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;
A5: k in NAT by ORDINAL1:def 12;
    per cases by A1,A4,NAT_1:8;
    suppose
A6:   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,A6;
      then
A7:   R.k = (s@x).k by FINSEQ_1:def 7
        .= (s.k)@x by A3,A6,Def9;
      dom s = Seg (len s) by FINSEQ_1:def 3;
      then
A8:   k in dom s by A3,A5,A6;
      k <= len (s ^ <*f*>) by A4,Def9;
      then L.k = ((s ^ <*f*>).k)@x by A3,Def9;
      hence thesis by A7,A8,FINSEQ_1:def 7;
    end;
    suppose
A9:   k = len L;
      dom (<*f@x*>) = {1} by FINSEQ_1:2,def 8;
      then
A10:  1 in dom (<*f@x*>) by TARSKI:def 1;
      len (s@x) = len s by Def9;
      then
A11:  R.k = <*f@x*>.1 by A1,A9,A10,FINSEQ_1:def 7
        .= f@x by FINSEQ_1:def 8;
      dom (<*f*>) = {1} by FINSEQ_1:2,def 8;
      then 1 in dom (<*f*>) by TARSKI:def 1;
      then
A12:  (s ^ <*f*>).k = <*f*>.1 by A1,A9,FINSEQ_1:def 7
        .= f by FINSEQ_1:def 8;
      k <= len (s ^ <*f*>) by A4,Def9;
      hence thesis by A3,A11,A12,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,FINSEQ_1:14;
end;

theorem Th34:
  for X being non empty set, s being FinSequence of bspace(X), x
  being 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 being FinSequence of V, f being 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 being FinSequence of V holds Q[p] from IndSeqS(A1,A3);
  hence thesis;
end;

theorem Th35:
  for X being non empty set, l being Linear_Combination of bspace(
  X), x being 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 being set such that
A1: f in singletons(X) by XBOOLE_0:def 1;
  ex g being Subset of X st g = f & g is 1-element by A1;
  hence thesis;
end;

end;

theorem 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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 NAT by ORDINAL1:def 12;
            then
A23:        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,A22;
            then
A24:        (m (#) F).k = m.(F/.k)*(F/.k) by VECTSP_6:def 5;
            reconsider Fk = F/.k as Subset of X;
A25:        Carrier m c= C \ {f} by VECTSP_6:def 4;
            dom F = Seg (len F) by FINSEQ_1:def 3;
            then
A26:        k in dom F by A19,A21,A22;
            then
A27:        F/.k = F.k by PARTFUN1:def 6;
            then m.(F/.k) = 1_Z_2 by A17,A26,Th35,FUNCT_1:3;
            then
A28:        (m (#) F).k = Fk by A24,VECTSP_1:def 17;
A29:        F/.k in Carrier m by A17,A26,A27,FUNCT_1:3;
            then
A30:        Fk in C by A25,XBOOLE_0:def 5;
A31:        Fk <> f
            proof
              assume Fk = f;
              then not f in {f} by A29,A25,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,A28,A31,A30;
            hence thesis by A23,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,FINSEQ_1:14;
        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
A32:  s@x = t@x + u@x by Th15;
      s@x = 0.Z_2 by A1,Def3;
      hence thesis by A8,A32,A13,A6,Th5,RLVECT_1:4;
    end;
    hence thesis by VECTSP_7:def 1;
  end;
end;

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

theorem Th38:
  for X being finite set, A being Subset of X ex l being
  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 being 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 being 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 being 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,XBOOLE_0:def 7
        .= B \/ {x};
      hence thesis;
    end;
  end;
A9: A is finite;
  P[A] from FINSET_1:sch 2(A9,A1,A2);
  hence thesis;
end;

theorem Th39:
  for X being finite set holds Lin(singletons(X)) = bspace(X)
proof
  let X be finite set;
  set V = bspace(X);
  set S = singletons(X);
  for v being Element of V holds v in Lin(S)
  proof
    let v be Element of V;
    reconsider f = v as Subset of X;
    consider A being set such that
A1: A c= X and
A2: f = A;
    reconsider A as Subset of X by A1;
    ex l being 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 Th40:
  for X being 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
  card (singletons X) = card X
proof
  defpred P[set,set] means $1 in X & $2 = {$1};
A1: for x being set st x in X holds ex y being set st P[x,y];
  consider f being Function such that
A2: dom f = X and
A3: for x being set 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 set;
      assume y in rng f;
      then consider x being set 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 set such that
A8: y in singletons(X);
    reconsider X as non empty set by A8;
 ex z being Subset of X st y = z & z is 1-element by A8;
    then reconsider y as 1-element Subset of X;
    consider x being 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 set 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
  card [#](bspace X) = exp(2,card(X)) by CARD_2:31;

theorem
  dim bspace {} = 0
proof
  card [#]bspace {} = 1 by CARD_2:42,ZFMISC_1:1;
  hence thesis by RANKNULL:5;
end;