:: The Vector Space of Subsets of a Set Based on Disjoint Union
::  by Jesse Alama
::
:: Received October 9, 2007
:: Copyright (c) 2007 Association of Mizar Users

environ

 vocabularies FINSET_1, BSPACE, FUNCT_1, CARD_1, SUBSET_1, TARSKI, BOOLE,
      RELAT_1, NAT_1, GROUP_1, FINSEQ_1, FINSEQ_2, QC_LANG1, BINOP_1, VECTSP_1,
      RLVECT_1, RLVECT_3, RLVECT_2, SEQ_1, FINSEQ_4, FUNCT_4, ORDINAL2,
      MATRLIN, VECTSP_9, INT_3, REALSET1, ARYTM;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, DOMAIN_1, RELSET_1,
      FUNCT_1, NUMBERS, NAT_1, INT_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_7,
      XXREAL_0, CARD_1, FINSET_1, FINSEQ_1, FINSEQOP, CARD_2, REALSET1,
      STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, VECTSP_6, VECTSP_7,
      VECTSP_9, INT_3, RANKNULL;
 constructors NAT_1, FINSEQOP, HAHNBAN, VECTSP_7, VECTSP_9, REALSET1, WELLORD2,
      NAT_D, FUNCT_7, BINOP_1, CARD_2, RANKNULL, INT_3, GR_CY_1, XXREAL_0;
 registrations RELAT_1, STRUCT_0, CARD_1, FINSET_1, FINSEQ_1, REALSET1,
      SUBSET_1, XBOOLE_0, VECTSP_1, ORDINAL1, XREAL_0, INT_1;
 requirements NUMERALS, BOOLE, ARITHM, SUBSET, REAL;
 definitions TARSKI, FUNCT_1, FINSEQ_1, CARD_1, VECTSP_6, XBOOLE_0, VECTSP_1,
      RLVECT_1, STRUCT_0, FINSEQ_2, BINOP_1, INT_3, ALGSTR_0;
 theorems TARSKI, ZFMISC_1, FINSET_1, FINSEQ_1, FUNCT_1, VECTSP_7, VECTSP_9,
      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, REALSET1,
      ORDINAL1, PARTFUN1, FINSEQ_3;
 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,
  d for Element of S,
  i for Element of NAT,
  p for FinSequence,
  b,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:13;
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:14;
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;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: The two-element field Z_2
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

begin

definition
  func Z_2 -> Field equals

  INT.Ring(2);
  coherence by INT_2:44,INT_3:22;
end;

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

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

theorem Th5:
  0.Z_2 = 0 by FUNCT_7:def 1,GR_CY_1:12;

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

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 5
    .= 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:88,TARSKI:def 2;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Set-theoretical Preliminaries
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

begin

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:88,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:88,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:88,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
A4:   not x in v by A1,XBOOLE_0:1;
A5:   u@x = 1.Z_2 by A3,Def3;
      v@x = 0.Z_2 by A4,Def3;
      hence thesis by A2,A5,RLVECT_1:10;
    end;
    suppose
A6:   not x in u;
      then
A7:   x in v by A1,XBOOLE_0:1;
A8:   u@x = 0.Z_2 by A6,Def3;
      v@x = 1.Z_2 by A7,Def3;
      hence thesis by A2,A8,RLVECT_1:10;
    end;
  end;
  suppose
A9: not x in u \+\ v;
    then
A10: (u \+\ v)@x = 0.Z_2 by Def3;
    per cases;
    suppose
A11:  x in u;
      then
A12:  x in v by A9,XBOOLE_0:1;
      u@x = 1.Z_2 by A11,Def3;
      hence thesis by A10,A12,Def3,Th7;
    end;
    suppose
A13:  not x in u;
      then
A14:  not x in v by A9,XBOOLE_0:1;
A15:  u@x = 0.Z_2 by A13,Def3;
      v@x = 0.Z_2 by A14,Def3;
      hence thesis by A10,A15,RLVECT_1:10;
    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 such that
A2:   y in X;
      X@y = 1.Z_2 by A2,Def3;
      then Y@y = 1.Z_2 by A1;
      hence thesis by Def3;
    end;
    let y be set such that
A3: y in Y;
    Y@y = 1.Z_2 by A3,Def3;
    then X@y = 1.Z_2 by A1;
    hence thesis by Def3;
  end;
end;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: The Boolean Bector Space of Subsets of a Set
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

begin

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 such that
A2:   x in bool X and
A3:   y in bool X;
      reconsider x,y as Subset of X by A2,A3;
      set z = x \+\ y;
      take z;
      thus thesis;
    end;
    consider f being Function of [:bool X,bool X:],bool X such that
A4: 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;
A5: for c,d being Subset of X holds f.(c,d) = c \+\ d
    proof
      let c,d be Subset of X;
      consider a,b being Subset of X such that
A6:   c = a and
A7:   d = b and
A8:   f.(c,d) = a \+\ b by A4;
      thus thesis by A6,A7,A8;
    end;
    take f;
    thus thesis by A5;
  end;
  uniqueness
  proof
    let f,g be BinOp of bool X such that
A9: for c,d being Subset of X holds f.(c,d) = c \+\ d and
A10: for c,d being Subset of X holds g.(c,d) = c \+\ d;
    dom f = [:bool X,bool X:] by FUNCT_2:def 1;
    then
A11: dom f = dom g by FUNCT_2:def 1;
    for x being set st x in dom f holds f.x = g.x
    proof
      let x be set such that
A12:  x in dom f;
      consider y,z being set such that
A13:  y in bool X and
A14:  z in bool X and
A15:  x = [y,z] by A12,ZFMISC_1:def 2;
      reconsider y as Subset of X by A13;
      reconsider z as Subset of X by A14;
      f.(y,z) = y \+\ z & g.(y,z) = y \+\ z by A9,A10;
      hence thesis by A15;
    end;
    hence thesis by A11,FUNCT_1:9;
  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:88,TARSKI:def 2;
  suppose a = 0.Z_2;
    then a \*\ (c \+\ d) = {}X & a \*\ c = {}X & a \*\ d = {}X by Def4;
    hence thesis;
  end;
  suppose a = 1.Z_2;
    then a \*\ (c \+\ d) = c \+\ d & a \*\ c = c & a \*\ d = d by Def4;
    hence thesis;
  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:88,TARSKI:def 2;
  suppose
A1: a = 0.Z_2;
    then a \*\ c = {}X by Def4;
    hence thesis by A1,RLVECT_1:10;
  end;
  suppose
A2: a = 1.Z_2;
    per cases by Th5,Th6,CARD_1:88,TARSKI:def 2;
    suppose
A3:   b = 0.Z_2;
      then b \*\ c = {}X by Def4;
      hence thesis by A3,RLVECT_1:10;
    end;
    suppose
A4:   b = 1.Z_2;
      then
A5:   b \*\ c = c by Def4;
      c \+\ c = {}X by XBOOLE_1:92;
      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:88,TARSKI:def 2;
  suppose
A1: a = 0.Z_2;
    then
A2: a*b = 0.Z_2 by VECTSP_1:39;
    a \*\ (b \*\ c) = {}X by A1,Def4;
    hence thesis by A2,Def4;
  end;
  suppose
A3: a = 1.Z_2;
    then a \*\ (b \*\ c) = b \*\ c by Def4;
    hence thesis by A3,VECTSP_1:def 16;
  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 x as Element of Z_2 by A2;
      reconsider y as Subset of X by A3;
      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);
A5: 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;
      consider a' being Element of Z_2, c' being Subset of X such that
A6:   a = a' and
A7:   c = c' and
A8:   f.(a,c) = a' \*\ c' by A4;
      thus thesis by A6,A7,A8;
    end;
    take f;
    thus thesis by A5;
  end;
  uniqueness
  proof
    let f,g be Function of [:the carrier of Z_2,bool X:],bool X such that
A9: for a being Element of Z_2, c being Subset of X
    holds f.(a,c) = a \*\ c and
A10: for a being Element of Z_2, c being Subset of X holds g.(a,c) = a \*\ c;
    dom f = [:the carrier of Z_2,bool X:] by FUNCT_2:def 1;
    then
A11: dom f = dom g by FUNCT_2:def 1;
    for x being set st x in dom f holds f.x = g.x
    proof
      let x be set such that
A12:  x in dom f;
      consider y,z being set such that
A13:  y in the carrier of Z_2 and
A14:  z in bool X and
A15:  x = [y,z] by A12,ZFMISC_1:def 2;
      reconsider y as Element of Z_2 by A13;
      reconsider z as Subset of X by A14;
      f.(y,z) = y \*\ z & g.(y,z) = y \*\ z by A9,A10;
      hence thesis by A15;
    end;
    hence thesis by A11,FUNCT_1:9;
  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
A1: a = A & b = B & c = C;
  thus a+(b+c) = A \+\ (B \+\ C)
  proof
    b+c = B \+\ C by A1,Def5;
    hence thesis by A1,Def5;
  end;
  thus (a+b)+c = (A \+\ B) \+\ C
  proof
    a+b = A \+\ B by A1,Def5;
    hence thesis by A1,Def5;
  end;
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;
  thus (a*x)+(b*y) = (a \*\ c) \+\ (b \*\ d)
  proof
A3: a*x = a \*\ c by A1,Def6;
    b*y = b \*\ d by A2,Def6;
    hence thesis by A3,Def5;
  end;
  thus a*(x+y) = a \*\ (c \+\ d)
  proof
A4: x+y = c \+\ d by A1,A2,Def5;
    thus thesis by A4,Def6;
  end;
  thus (a+b)*x = (a+b) \*\ c by A1,Def6;
  thus (a*b)*x = (a*b) \*\ c by A1,Def6;
  thus a*(b*x) = a \*\ (b \*\ c)
  proof
    b*x = b \*\ c by A1,Def6;
    hence thesis by Def6;
  end;
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;
A1: A \+\ A = {}X by XBOOLE_1:92;
  take x;
  thus thesis by A1,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 VectSp-like
proof
  let a,b be Element of Z_2, x,y be Element of bspace(X);
  thus a*(x+y) = (a*x)+(a*y) by Th25;
  thus (a+b)*x = (a*x)+(b*x) by Th26;
  thus (a*b)*x = a*(b*x) by Th27;
  thus (1.Z_2)*x = x by Th28;
end;

registration
  let X be set;
  cluster bspace(X) -> VectSp-like Abelian right_complementable
    add-associative right_zeroed;
  coherence by Th21,Th22,Th23,Th24,Th29;
end;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: The Linear Independence and Linear Span of Singleton Subsets
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

begin

definition
  let X be set;
  attr X is Singleton means
  :Def8:
  X is non empty trivial;
end;

registration
  cluster Singleton -> non empty trivial set;
  coherence by Def8;
  cluster non empty trivial -> Singleton set;
  coherence by Def8;
end;

definition
  let X be set, f be Subset of X;
  redefine attr f is Singleton means
  :Def9:
  ex x being set st x in X & f = {x};
  compatibility
  proof
    thus f is Singleton implies ex x being set st x in X & f = {x}
    proof
      assume f is Singleton;
      then f is non empty trivial;
      then consider x being set such that
A1:   f = {x} by REALSET1:def 4;
      take x;
      x in f by A1,TARSKI:def 1;
      hence x in X;
      thus thesis by A1;
    end;
    thus thesis;
  end;
end;

definition
  let X be set;
  func singletons(X) equals

  { f where f is Subset of X : f is Singleton };
  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 such that
A1:   f in S;
      consider g being Subset of X such that
A2:   f = g and g is Singleton by A1;
      reconsider f as Subset of X by A2;
      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
    consider x being 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 Singleton
proof
  let X be non empty set, f be Subset of X such that
A1: f is Element of singletons(X);
  f in singletons(X) by A1;
  then consider g being Subset of X such that
A2: g = f and
A3: g is Singleton;
  thus thesis by A2,A3;
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
  :Def11:
  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 such that
A4:   1 <= j and
A5:   j <= len s;
      j in dom p by A4,A5,FINSEQ_3:27,A1;
      hence thesis by A2;
    end;
    rng p c= the carrier of Z_2
    proof
      let y be set such that
A6:   y in rng p;
      consider a being set such that
A7:   a in dom p and
A8:   p.a = y by A6,FUNCT_1:def 5;
      p.a = (s.a)@x by A2,A7;
      hence thesis by A8;
    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
A9: len f = len s & for j being Nat st 1 <= j & j <= len s
    holds f.j = (s.j)@x and
A10: len g = len s & 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
A11:  1 <= k and
A12:  k <= len f;
      f.k = (s.k)@x & g.k = (s.k)@x by A9,A10,A11,A12;
      hence thesis;
    end;
    hence thesis by A9,A10,FINSEQ_1:18;
  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 Def11
    .= 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 u' = u, v' = v as Subset of X;
  (u + v)@x = (u' \+\ v')@x by Def5
    .= (u'@x) + (v'@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 Def11
    .= (len s) + (len <*f*>) by FINSEQ_1:35
    .= (len s) + 1 by FINSEQ_1:56;
A2: len ((s@x) ^ <*f@x*>) = (len (s@x)) + (len <*f@x*>) by FINSEQ_1:35
    .= (len s) + (len <*f@x*>) by Def11
    .= (len s) + 1 by FINSEQ_1:56;
  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 13;
    per cases by A1,A4,NAT_1:8;
    suppose
A6:   k <= len s;
      k <= len (s ^ <*f*>) by A4,Def11;
      then
A7:   L.k = ((s ^ <*f*>).k)@x by A3,Def11;
      dom (s@x) = Seg (len (s@x)) by FINSEQ_1:def 3
        .= Seg (len s) by Def11;
      then k in dom (s@x) by A3,A5,A6;
      then
A8:   R.k = (s@x).k by FINSEQ_1:def 7
        .= (s.k)@x by A3,A6,Def11;
      dom s = Seg (len s) by FINSEQ_1:def 3;
      then k in dom s by A3,A5,A6;
      hence thesis by A7,A8,FINSEQ_1:def 7;
    end;
    suppose
A9:   k = len L;
A10:  k <= len (s ^ <*f*>) by A4,Def11;
A11:  len (s@x) = len s by Def11;
      dom (<*f@x*>) = {1} by FINSEQ_1:4,def 8;
      then 1 in dom (<*f@x*>) by TARSKI:def 1;
      then
A12:  R.k = <*f@x*>.1 by A1,A9,A11,FINSEQ_1:def 7
        .= f@x by FINSEQ_1:def 8;
      dom (<*f*>) = {1} by FINSEQ_1:4,def 8;
      then 1 in dom (<*f*>) by TARSKI:def 1;
      then (s ^ <*f*>).k = <*f*>.1 by A1,A9,FINSEQ_1:def 7
        .= f by FINSEQ_1:def 8;
      hence thesis by A3,A10,A12,Def11;
    end;
  end;
  hence thesis by A1,A2,FINSEQ_1:18;
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
    set e = <*>V;
    reconsider z = 0.V as Subset of X;
A2: Sum e = 0.V by RLVECT_1:60;
A3: e@x = <*>Z_2 by Th31;
    z@x = 0.Z_2 by Def3;
    hence thesis by A2,A3,RLVECT_1:60;
  end;
A4: 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
A5: Q[p];
    (Sum (p ^ <*f*>))@x = ((Sum p) + (Sum <*f*>))@x by RLVECT_1:58
      .= ((Sum p) + f)@x by RLVECT_1:61
      .= (Sum p)@x + f@x by Th32
      .= Sum (p@x) + Sum (<*f@x*>) by A5,RLVECT_1:61
      .= Sum (p@x ^ <*f@x*>) by RLVECT_1:58
      .= Sum ((p ^ <*f*>)@x) by Th33;
    hence thesis;
  end;
  for p being FinSequence of V holds Q[p] from IndSeqS(A1,A4);
  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) such that
A1: x in Carrier l;
  l.x <> 0.Z_2 by A1,VECTSP_6:20;
  hence thesis by Th5,Th6,CARD_1:88,TARSKI:def 2;
end;

theorem Th36:
  singletons {} = {}
proof
  set X = {};
  assume singletons(X) <> {};
  then consider f being set such that
A1: f in singletons(X) by XBOOLE_0:def 1;
  consider g being Subset of X such that g = f and
A2: g is Singleton by A1;
  consider x being set such that
A3: x in X and g = {x} by A2;
  thus thesis by A3;
end;

theorem Th37:
  singletons(X) is linearly-independent
proof
  per cases;
  suppose
A1: X is empty;
    {} = {}(the carrier of bspace(X));
    hence thesis by A1,Th36,VECTSP_7:4;
  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
A2:   Sum l = 0.V;
      set C = Carrier l;
      reconsider s = Sum l as Subset of X;
      assume C <> {};
      then consider f being Element of V such that
A3:   f in C by SUBSET_1:10;
      reconsider f as Subset of X;
      C c= S by VECTSP_6:def 7;
      then f is Singleton by A3,Th30;
      then consider x being set such that
A4:   x in X and
A5:   f = {x} by Def9;
      x in f by A5,TARSKI:def 1;
      then
A6:   f@x = 1.Z_2 by Def3;
      reconsider x as Element of X by A4;
A7:   s@x = 0.Z_2 by A2,Def3;
A8:   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
A9:     g <> f and
A10:    g in C;
        C c= S by VECTSP_6:def 7;
        then g is Singleton by A10,Th30;
        then consider y being set such that
A11:    y in X and
A12:    g = {y} by Def9;
        reconsider y as Element of X by A11;
        now
          assume g@x <> 0.Z_2;
          then x in {y} by A12,Def3;
          hence contradiction by A5,A9,A12,TARSKI:def 1;
        end;
        hence thesis;
      end;
      reconsider g = f as Element of V;
      reconsider m = l!(C \ {g}) as Linear_Combination of C \ {g};
      reconsider n = l!{g} as Linear_Combination of {g};
      reconsider t = Sum m, u = Sum n as Subset of X;
A13:  l!(Carrier l) = l by RANKNULL:24;
A14:  {g} c= Carrier l by A3,ZFMISC_1:37;
      reconsider l as Linear_Combination of C by A13;
      l = n + m by A14,RANKNULL:27;
      then Sum l = (Sum m) + (Sum n) by VECTSP_6:77;
      then s = t \+\ u by Def5;
      then
A15:  s@x = t@x + u@x by Th15;
A16:  t@x = 0
      proof
A17:    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
A18:      rng F = Carrier m;
          set L = (m (#) F)@x;
          set R = (len F) |-> 0.Z_2;
A19:      len (m (#) F) = len F by VECTSP_6:def 8;
          then
A20:      len L = len F by Def11;
          dom R = Seg (len F) by FUNCOP_1:19;
          then
A21:      len L = len R by A20,FINSEQ_1:def 3;
          for k being Nat st 1 <= k & k <= len L holds L.k = R.k
          proof
            let k be Nat such that
A22:        1 <= k and
A23:        k <= len L;
            len (m (#) F) = len F by VECTSP_6:def 8;
            then
A24:        dom (m (#) F) = Seg (len F) by FINSEQ_1:def 3;
A25:        k in NAT by ORDINAL1:def 13;
            then k in dom (m (#) F) by A20,A22,A23,A24;
            then
A26:        (m (#) F).k = m.(F/.k)*(F/.k) by VECTSP_6:def 8;
            dom F = Seg (len F) by FINSEQ_1:def 3;
            then
A27:        k in dom F by A20,A22,A23,A25;
            then
A28:        F/.k = F.k by PARTFUN1:def 8;
            then
A29:        F/.k in Carrier m by A18,A27,FUNCT_1:12;
            reconsider Fk = F/.k as Subset of X;
            m.(F/.k) = 1_Z_2 by A18,A27,A28,Th35,FUNCT_1:12;
            then
A30:        (m (#) F).k = Fk by A26,VECTSP_1:def 26;
A31:        Carrier m = C \ {f}
            proof
              thus Carrier m c= C \ {f} by VECTSP_6:def 7;
              thus C \ {f} c= Carrier m
              proof
                let y be set such that
A32:            y in C \ {f};
A33:            y in C by A32,XBOOLE_0:def 4;
                reconsider y as Element of V by A32;
                now
                  assume
A34:              not y in Carrier m;
                  m.y = l.y by A32,RANKNULL:25;
                  then l.y = 0.Z_2 by A34;
                  hence contradiction by A33,VECTSP_6:20;
                end;
                hence thesis;
              end;
            end;
A35:        Fk <> f
            proof
              assume Fk = f;
              then not f in {f} by A29,A31,XBOOLE_0:def 4;
              hence contradiction by TARSKI:def 1;
            end;
A36:        Fk in C by A29,A31,XBOOLE_0:def 4;
A37:        L.k = ((m (#) F).k)@x by A19,A20,A22,A23,Def11
              .= 0.Z_2 by A8,A30,A35,A36;
            k in Seg (len F) by A20,A22,A23,A25;
            hence thesis by A37,FUNCOP_1:13;
          end;
          hence thesis by A21,FINSEQ_1:18;
        end;
        consider F being FinSequence of V such that
A38:    F is one-to-one and
A39:    rng F = Carrier m and
A40:    t = Sum (m (#) F) by VECTSP_6:def 9;
A41:    (Sum (m (#) F))@x = Sum ((m (#) F)@x) by Th34;
        (m (#) F)@x = (len F) |-> 0.Z_2 by A17,A38,A39;
        hence thesis by A40,A41,Th5,MATRIX_3:13;
      end;
      u = f
      proof
A42:    Sum n = (n.g)*g by VECTSP_6:43;
        g in {g} by TARSKI:def 1;
        then
A43:    n.g = l.g by RANKNULL:25;
        l.g <> 0.Z_2 by A3,VECTSP_6:20;
        then
A44:    l.g = 1_Z_2 by Th5,Th6,CARD_1:88,TARSKI:def 2;
        thus thesis by A42,A43,A44,VECTSP_1:def 26;
      end;
      hence thesis by A6,A7,A15,A16,Th5,RLVECT_1:10;
    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 Th39:
  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: A is finite;
A2: P[{}]
  proof
    assume {} is Subset of X;
    reconsider l = ZeroLC(V) as Linear_Combination of S by VECTSP_6:26;
A3: Sum l = 0.V by VECTSP_6:41;
    take l;
    thus thesis by A3;
  end;
A4: 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
A5: P[B];
    assume
A6: 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
A7: Sum l = B by A5;
    per cases;
    suppose
A8:   x in B;
      take l;
      thus thesis by A7,A8,ZFMISC_1:46;
    end;
    suppose
A9:   not x in B;
      reconsider f = {x} as Element of V by A6,XBOOLE_1:11;
      reconsider g = f as Subset of X;
      reconsider z = ZeroLC(V) as Linear_Combination of {}V by VECTSP_6:26;
      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:169;
      then
A10:  m.f = 1_Z_2 by FUNCT_7:33;
A11:  B misses {x} by A9,ZFMISC_1:56;
      f in S;
      then {f} c= S by ZFMISC_1:37;
      then m is Linear_Combination of S by VECTSP_6:25;
      then reconsider n = l + m as Linear_Combination of S by VECTSP_6:52;
A12:  Sum n = (Sum l) + (Sum m) by VECTSP_6:77
        .= (Sum l) + (m.f)*f by VECTSP_6:43
        .= (Sum l) + f by A10,VECTSP_1:def 26
        .= B \+\ g by A7,Def5
        .= (B \/ {x}) \ (B /\ {x}) by XBOOLE_1:101
        .= (B \/ {x}) \ {} by A11,XBOOLE_0:def 7
        .= B \/ {x};
      take n;
      thus thesis by A12;
    end;
  end;
  P[A] from FINSET_1:sch 2(A1,A2,A4);
  hence thesis;
end;

theorem Th40:
  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;
    consider l being Linear_Combination of S such that
A3: Sum l = A by Th39;
    thus thesis by A2,A3,VECTSP_7:12;
  end;
  hence thesis by VECTSP_4:40;
end;

theorem Th41:
  for X being finite set holds singletons(X) is Basis of bspace(X)
proof
  let X be finite set;
A1: singletons(X) is linearly-independent by Th37;
  Lin(singletons(X)) = bspace(X) by Th40;
  hence thesis by A1,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);
A1: S is Basis of bspace(X) by Th41;
    thus thesis by A1,VECTSP_9:def 1;
  end;
end;

theorem
  Card (singletons X) = Card X
proof
  defpred P[set,set] means $1 in X & $2 = {$1};
A2: for x being set st x in X holds ex y being set st P[x,y];
  consider f being Function such that
A3: dom f = X and
A4: for x being set st x in X holds P[x,f.x] from CLASSES1:sch 1(A2);
A5: f is one-to-one
  proof
    let x1,x2 be set such that
A6: x1 in dom f and
A7: x2 in dom f and
A8: f.x1 = f.x2;
A9: P[x1,f.x1] by A3,A4,A6;
    P[x2,f.x2] by A3,A4,A7;
    hence thesis by A8,A9,ZFMISC_1:6;
  end;
  rng f = singletons(X)
  proof
    thus rng f c= singletons(X)
    proof
      let y be set such that
A10:  y in rng f;
      consider x being set such that
A11:  x in dom f and
A12:  y = f.x by A10,FUNCT_1:def 5;
A13:  f.x = {x} by A3,A4,A11;
      then reconsider fx = f.x as Subset of X by A3,A11,ZFMISC_1:37;
      fx is Singleton by A13;
      hence thesis by A12;
    end;
    let y be set such that
A14: y in singletons(X);
    consider z being Subset of X such that
A15: y = z and
A16: z is Singleton by A14;
    reconsider y as Subset of X by A15;
    consider x being set such that
A17: x in X and
A18: y = {x} by A15,A16,Def9;
    reconsider x as Element of X by A17;
    y = f.x by A4,A17,A18;
    hence thesis by A3,A17,FUNCT_1:12;
  end;
  then X,singletons(X) are_equipotent by A3,A5,WELLORD2:def 4;
  hence thesis by CARD_1:21;
end;

theorem
  Card [#](bspace X) = exp(2,Card(X)) by CARD_2:44;

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