:: BSPACE semantic presentation

begin

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

:: deftheorem  defines <*> BSPACE:def_1_:_
 for S being 1-sorted holds <*> S = <*> ([#] S);


theorem :: BSPACE:1
for S being 1-sorted
for i being Element of NAT
for p being FinSequence of S st i in dom p holds
p . i in S
proof
let S be 1-sorted ; ::_thesis: for i being Element of NAT
for p being FinSequence of S st i in dom p holds
p . i in S
let i be Element of NAT ; ::_thesis: for p being FinSequence of S st i in dom p holds
p . i in S
let p be FinSequence of S; ::_thesis: ( i in dom p implies p . i in S )
assume  i in dom p ; ::_thesis: p . i in S
hence  p . i in the carrier of S by FINSEQ_2:11; :: according to STRUCT_0:def_5 ::_thesis: verum
end;

theorem :: BSPACE:2
for S being 1-sorted
for p being FinSequence st ( for i being Nat st i in dom p holds
p . i in S ) holds
p is FinSequence of S
proof
let S be 1-sorted ; ::_thesis: for p being FinSequence st ( for i being Nat st i in dom p holds
p . i in S ) holds
p is FinSequence of S
let p be FinSequence; ::_thesis: ( ( for i being Nat st i in dom p holds
p . i in S ) implies p is FinSequence of S )
assume A1: for i being Nat st i in dom p holds
p . i in S ; ::_thesis: p is FinSequence of S
 for i being Nat st i in dom p holds
p . i in the carrier of S
proof
let i be Nat; ::_thesis: ( i in dom p implies p . i in the carrier of S )
assume  i in dom p ; ::_thesis: p . i in the carrier of S
then  p . i in S by A1;
hence  p . i in the carrier of S by STRUCT_0:def_5; ::_thesis: verum
end;
hence  p is FinSequence of S by FINSEQ_2:12; ::_thesis: verum
end;

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

begin

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

:: deftheorem  defines Z_2 BSPACE:def_2_:_
 Z_2 = INT.Ring 2;

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

theorem :: BSPACE:4
for a being Element of Z_2 holds
( a = 0 or a = 1 ) by CARD_1:50, TARSKI:def_2;

theorem Th5: :: BSPACE:5
0. Z_2 = 0
proof
 0 in 2 by NAT_1:44;
hence  0. Z_2 = 0 by FUNCT_7:def_1; ::_thesis: verum
end;

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

theorem Th7: :: BSPACE:7
(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  (1. Z_2) + (1. Z_2) = 0. Z_2 by FUNCT_7:def_1; ::_thesis: verum
end;

theorem :: BSPACE:8
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

definition
let X, x be set ;
funcX @ x ->  Element of Z_2 equals :Def3: :: BSPACE:def 3
 1. Z_2 if x in X
otherwise  0. Z_2;
coherence
 ( ( x in X implies 1. Z_2 is Element of Z_2 ) & ( not x in X implies 0. Z_2 is Element of Z_2 ) ) ;
consistency
 for b1 being Element of Z_2 holds verum ;
end;

:: deftheorem Def3 defines @ BSPACE:def_3_:_
 for X, x being set holds
( ( x in X implies X @ x = 1. Z_2 ) & ( not x in X implies X @ x = 0. Z_2 ) );

theorem :: BSPACE:9
for X, x being set holds
( X @ x = 1. Z_2 iff x in X ) by Def3;

theorem :: BSPACE:10
for X, x being set holds
( X @ x = 0. Z_2 iff not x in X ) by Def3;

theorem :: BSPACE:11
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 :: BSPACE:12
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 ; ::_thesis: ( X @ x = X @ y iff ( x in X iff y in X ) )
thus  ( X @ x = X @ y implies ( x in X iff y in X ) ) ::_thesis: not ( ( x in X implies y in X ) & ( y in X implies x in X ) & not X @ x = X @ y )
proof
assume A1: X @ x = X @ y ; ::_thesis: ( x in X iff y in X )
thus  ( x in X implies y in X ) ::_thesis: ( y in X implies x in X )
proof
assume  x in X ; ::_thesis: y in X
then  X @ x = 1. Z_2 by Def3;
hence  y in X by A1, Def3; ::_thesis: verum
end;
assume  y in X ; ::_thesis: x in X
then  X @ y = 1. Z_2 by Def3;
hence  x in X by A1, Def3; ::_thesis: verum
end;
assume A2: ( x in X iff y in X ) ; ::_thesis: X @ x = X @ y
percases ( X @ x = 0. Z_2 or X @ x = 1. Z_2 ) by Th5, Th6, CARD_1:50, TARSKI:def_2;
suppose X @ x = 0. Z_2 ; ::_thesis: X @ x = X @ y
hence  X @ x = X @ y by A2, Def3; ::_thesis: verum
end;
suppose X @ x = 1. Z_2 ; ::_thesis: X @ x = X @ y
hence  X @ x = X @ y by A2, Def3; ::_thesis: verum
end;
end;
end;

theorem :: BSPACE:13
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 ; ::_thesis: ( X @ x = Y @ x iff ( x in X iff x in Y ) )
thus  ( X @ x = Y @ x implies ( x in X iff x in Y ) ) ::_thesis: not ( ( x in X implies x in Y ) & ( x in Y implies x in X ) & not X @ x = Y @ x )
proof
assume A1: X @ x = Y @ x ; ::_thesis: ( x in X iff x in Y )
thus  ( x in X implies x in Y ) ::_thesis: ( x in Y implies x in X )
proof
assume  x in X ; ::_thesis: x in Y
then  X @ x = 1. Z_2 by Def3;
hence  x in Y by A1, Def3; ::_thesis: verum
end;
assume  x in Y ; ::_thesis: x in X
then  Y @ x = 1. Z_2 by Def3;
hence  x in X by A1, Def3; ::_thesis: verum
end;
thus  not ( ( x in X implies x in Y ) & ( x in Y implies x in X ) & not X @ x = Y @ x ) ::_thesis: verum
proof
assume A2: ( x in X iff x in Y ) ; ::_thesis: X @ x = Y @ x
percases ( X @ x = 0. Z_2 or X @ x = 1. Z_2 ) by Th5, Th6, CARD_1:50, TARSKI:def_2;
suppose X @ x = 0. Z_2 ; ::_thesis: X @ x = Y @ x
hence  X @ x = Y @ x by A2, Def3; ::_thesis: verum
end;
suppose X @ x = 1. Z_2 ; ::_thesis: X @ x = Y @ x
hence  X @ x = Y @ x by A2, Def3; ::_thesis: verum
end;
end;
end;
end;

theorem :: BSPACE:14
for x being set holds {} @ x = 0. Z_2 by Def3;

theorem Th15: :: BSPACE:15
for X being set
for u, v being Subset of X
for x being Element of X holds (u \+\ v) @ x = (u @ x) + (v @ x)
proof
let X be set ; ::_thesis: for u, v being Subset of X
for x being Element of X holds (u \+\ v) @ x = (u @ x) + (v @ x)
let u, v be Subset of X; ::_thesis: for x being Element of X holds (u \+\ v) @ x = (u @ x) + (v @ x)
let x be Element of X; ::_thesis: (u \+\ v) @ x = (u @ x) + (v @ x)
percases ( x in u \+\ v or not x in u \+\ v ) ;
supposeA1: x in u \+\ v ; ::_thesis: (u \+\ v) @ x = (u @ x) + (v @ x)
then A2: (u \+\ v) @ x = 1. Z_2 by Def3;
percases ( x in u or not x in u ) ;
supposeA3: x in u ; ::_thesis: (u \+\ v) @ x = (u @ x) + (v @ x)
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  (u \+\ v) @ x = (u @ x) + (v @ x) by A2, A4, RLVECT_1:4; ::_thesis: verum
end;
supposeA5: not x in u ; ::_thesis: (u \+\ v) @ x = (u @ x) + (v @ x)
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  (u \+\ v) @ x = (u @ x) + (v @ x) by A2, A6, RLVECT_1:4; ::_thesis: verum
end;
end;
end;
supposeA7: not x in u \+\ v ; ::_thesis: (u \+\ v) @ x = (u @ x) + (v @ x)
then A8: (u \+\ v) @ x = 0. Z_2 by Def3;
percases ( x in u or not x in u ) ;
suppose x in u ; ::_thesis: (u \+\ v) @ x = (u @ x) + (v @ x)
then  ( x in v & u @ x = 1. Z_2 ) by A7, Def3, XBOOLE_0:1;
hence  (u \+\ v) @ x = (u @ x) + (v @ x) by A8, Def3, Th7; ::_thesis: verum
end;
supposeA9: not x in u ; ::_thesis: (u \+\ v) @ x = (u @ x) + (v @ x)
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  (u \+\ v) @ x = (u @ x) + (v @ x) by A8, A10, RLVECT_1:4; ::_thesis: verum
end;
end;
end;
end;
end;

theorem :: BSPACE:16
for X, Y being set holds
( X = Y iff for x being set holds X @ x = Y @ x )
proof
let X, Y be set ; ::_thesis: ( X = Y iff for x being set holds X @ x = Y @ x )
thus  ( X = Y implies for x being set holds X @ x = Y @ x ) ; ::_thesis: ( ( for x being set holds X @ x = Y @ x ) implies X = Y )
thus  ( ( for x being set holds X @ x = Y @ x ) implies X = Y ) ::_thesis: verum
proof
assume A1: for x being set holds X @ x = Y @ x ; ::_thesis: X = Y
thus  X c= Y :: according to XBOOLE_0:def_10 ::_thesis: Y c= X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X or y in Y )
assume  y in X ; ::_thesis: y in Y
then  X @ y = 1. Z_2 by Def3;
then  Y @ y = 1. Z_2 by A1;
hence  y in Y by Def3; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in X )
assume  y in Y ; ::_thesis: y in X
then  Y @ y = 1. Z_2 by Def3;
then  X @ y = 1. Z_2 by A1;
hence  y in X by Def3; ::_thesis: verum
end;
end;

begin

definition
let X be set ;
let a be Element of Z_2;
let c be Subset of X;
funca \*\ c ->  Subset of X equals :Def4: :: BSPACE:def 4
c if a = 1. Z_2
{} X if a = 0. Z_2
;
consistency
 for b1 being Subset of X st a = 1. Z_2 & a = 0. Z_2 holds
( b1 = c iff b1 = {} X ) ;
coherence
 ( ( a = 1. Z_2 implies c is Subset of X ) & ( a = 0. Z_2 implies {} X is Subset of X ) ) ;
end;

:: deftheorem Def4 defines \*\ BSPACE:def_4_:_
 for X being set
for a being Element of Z_2
for c being Subset of X holds
( ( a = 1. Z_2 implies a \*\ c = c ) & ( a = 0. Z_2 implies a \*\ c = {} X ) );

definition
let X be set ;
func bspace-sum X ->  BinOp of (bool X) means :Def5: :: BSPACE:def 5
 for c, d being Subset of X holds it . (c,d) = c \+\ d;
existence
 ex b1 being BinOp of (bool X) st
for c, d being Subset of X holds b1 . (c,d) = c \+\ d
proof
defpred S1[ 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 holds
ex z being set st
( z in bool X & S1[x,y,z] )
proof
let x, y be set ; ::_thesis: ( x in bool X & y in bool X implies ex z being set st
( z in bool X & S1[x,y,z] ) )
assume  ( x in bool X & y in bool X ) ; ::_thesis: ex z being set st
( z in bool X & S1[x,y,z] )
then reconsider x = x, y = y as Subset of X ;
set z = x \+\ y;
take  x \+\ y ; ::_thesis: ( x \+\ y in bool X & S1[x,y,x \+\ y] )
thus  ( x \+\ y in bool X & S1[x,y,x \+\ y] ) ; ::_thesis: verum
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
S1[x,y,f . (x,y)] from BINOP_1:sch_1(A1);
reconsider f = f as BinOp of (bool X) ;
take  f ; ::_thesis: for c, d being Subset of X holds f . (c,d) = c \+\ d
 for c, d being Subset of X holds f . (c,d) = c \+\ d
proof
let c, d be Subset of X; ::_thesis: f . (c,d) = c \+\ d
 ex a, b being Subset of X st
( c = a & d = b & f . (c,d) = a \+\ b ) by A2;
hence  f . (c,d) = c \+\ d ; ::_thesis: verum
end;
hence  for c, d being Subset of X holds f . (c,d) = c \+\ d ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (bool X) st ( for c, d being Subset of X holds b1 . (c,d) = c \+\ d ) & ( for c, d being Subset of X holds b2 . (c,d) = c \+\ d ) holds
b1 = b2
proof
let f, g be BinOp of (bool X); ::_thesis: ( ( 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 ) implies f = g )
assume 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 ) ) ; ::_thesis: f = g
A4: for x being set st x in dom f holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume  x in dom f ; ::_thesis: f . x = g . x
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 = z as Subset of X by A6;
reconsider y = y as Subset of X by A5;
 ( f . (y,z) = y \+\ z & g . (y,z) = y \+\ z ) by A3;
hence  f . x = g . x by A7; ::_thesis: verum
end;
 dom f = [:(bool X),(bool X):] by FUNCT_2:def_1;
then  dom f = dom g by FUNCT_2:def_1;
hence  f = g by A4, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines bspace-sum BSPACE:def_5_:_
 for X being set
for b2 being BinOp of (bool X) holds
( b2 = bspace-sum X iff for c, d being Subset of X holds b2 . (c,d) = c \+\ d );

theorem Th17: :: BSPACE:17
for X being set
for a being Element of Z_2
for c, d being Subset of X holds a \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d)
proof
let X be set ; ::_thesis: for a being Element of Z_2
for c, d being Subset of X holds a \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d)
let a be Element of Z_2; ::_thesis: for c, d being Subset of X holds a \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d)
let c, d be Subset of X; ::_thesis: a \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d)
percases ( a = 0. Z_2 or a = 1. Z_2 ) by Th5, Th6, CARD_1:50, TARSKI:def_2;
supposeA1: a = 0. Z_2 ; ::_thesis: a \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d)
then  ( a \*\ (c \+\ d) = {} X & a \*\ c = {} X ) by Def4;
hence  a \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d) by A1, Def4; ::_thesis: verum
end;
supposeA2: a = 1. Z_2 ; ::_thesis: a \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d)
then  ( a \*\ (c \+\ d) = c \+\ d & a \*\ c = c ) by Def4;
hence  a \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d) by A2, Def4; ::_thesis: verum
end;
end;
end;

theorem Th18: :: BSPACE:18
for X being set
for a, b being Element of Z_2
for c being Subset of X holds (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c)
proof
let X be set ; ::_thesis: for a, b being Element of Z_2
for c being Subset of X holds (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c)
let a, b be Element of Z_2; ::_thesis: for c being Subset of X holds (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c)
let c be Subset of X; ::_thesis: (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c)
percases ( a = 0. Z_2 or a = 1. Z_2 ) by Th5, Th6, CARD_1:50, TARSKI:def_2;
supposeA1: a = 0. Z_2 ; ::_thesis: (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c)
then  a \*\ c = {} X by Def4;
hence  (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c) by A1, RLVECT_1:4; ::_thesis: verum
end;
supposeA2: a = 1. Z_2 ; ::_thesis: (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c)
percases ( b = 0. Z_2 or b = 1. Z_2 ) by Th5, Th6, CARD_1:50, TARSKI:def_2;
supposeA3: b = 0. Z_2 ; ::_thesis: (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c)
then  b \*\ c = {} X by Def4;
hence  (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c) by A3, RLVECT_1:4; ::_thesis: verum
end;
supposeA4: b = 1. Z_2 ; ::_thesis: (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c)
A5: c \+\ c = {} X by XBOOLE_1:92;
 b \*\ c = c by A4, Def4;
hence  (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c) by A2, A4, A5, Def4, Th7; ::_thesis: verum
end;
end;
end;
end;
end;

theorem :: BSPACE:19
for X being set
for c being Subset of X holds (1. Z_2) \*\ c = c by Def4;

theorem Th20: :: BSPACE:20
for X being set
for a, b being Element of Z_2
for c being Subset of X holds a \*\ (b \*\ c) = (a * b) \*\ c
proof
let X be set ; ::_thesis: for a, b being Element of Z_2
for c being Subset of X holds a \*\ (b \*\ c) = (a * b) \*\ c
let a, b be Element of Z_2; ::_thesis: for c being Subset of X holds a \*\ (b \*\ c) = (a * b) \*\ c
let c be Subset of X; ::_thesis: a \*\ (b \*\ c) = (a * b) \*\ c
percases ( a = 0. Z_2 or a = 1. Z_2 ) by Th5, Th6, CARD_1:50, TARSKI:def_2;
supposeA1: a = 0. Z_2 ; ::_thesis: a \*\ (b \*\ c) = (a * b) \*\ c
then  a \*\ (b \*\ c) = {} X by Def4;
hence  a \*\ (b \*\ c) = (a * b) \*\ c by A1, Def4, VECTSP_1:7; ::_thesis: verum
end;
supposeA2: a = 1. Z_2 ; ::_thesis: a \*\ (b \*\ c) = (a * b) \*\ c
then  a \*\ (b \*\ c) = b \*\ c by Def4;
hence  a \*\ (b \*\ c) = (a * b) \*\ c by A2, VECTSP_1:def_6; ::_thesis: verum
end;
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: :: BSPACE:def 6
 for a being Element of Z_2
for c being Subset of X holds it . (a,c) = a \*\ c;
existence
 ex b1 being Function of [: the carrier of Z_2,(bool X):],(bool X) st
for a being Element of Z_2
for c being Subset of X holds b1 . (a,c) = a \*\ c
proof
defpred S1[ set , set , set ] means  ex a being Element of Z_2 ex 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 holds
ex z being set st
( z in bool X & S1[x,y,z] )
proof
let x, y be set ; ::_thesis: ( x in the carrier of Z_2 & y in bool X implies ex z being set st
( z in bool X & S1[x,y,z] ) )
assume that
A2: x in the carrier of Z_2 and
A3: y in bool X ; ::_thesis: ex z being set st
( z in bool X & S1[x,y,z] )
reconsider y = y as Subset of X by A3;
reconsider x = x as Element of Z_2 by A2;
set z = x \*\ y;
take  x \*\ y ; ::_thesis: ( x \*\ y in bool X & S1[x,y,x \*\ y] )
thus  ( x \*\ y in bool X & S1[x,y,x \*\ y] ) ; ::_thesis: verum
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
S1[x,y,f . (x,y)] from BINOP_1:sch_1(A1);
take  f ; ::_thesis: for a being Element of Z_2
for c being Subset of X holds f . (a,c) = a \*\ c
 for a being Element of Z_2
for c being Subset of X holds f . (a,c) = a \*\ c
proof
let a be Element of Z_2; ::_thesis: for c being Subset of X holds f . (a,c) = a \*\ c
let c be Subset of X; ::_thesis: f . (a,c) = a \*\ c
 ex a9 being Element of Z_2 ex c9 being Subset of X st
( a = a9 & c = c9 & f . (a,c) = a9 \*\ c9 ) by A4;
hence  f . (a,c) = a \*\ c ; ::_thesis: verum
end;
hence  for a being Element of Z_2
for c being Subset of X holds f . (a,c) = a \*\ c ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [: the carrier of Z_2,(bool X):],(bool X) st ( for a being Element of Z_2
for c being Subset of X holds b1 . (a,c) = a \*\ c ) & ( for a being Element of Z_2
for c being Subset of X holds b2 . (a,c) = a \*\ c ) holds
b1 = b2
proof
let f, g be Function of [: the carrier of Z_2,(bool X):],(bool X); ::_thesis: ( ( for a being Element of Z_2
for c being Subset of X holds f . (a,c) = a \*\ c ) & ( for a being Element of Z_2
for c being Subset of X holds g . (a,c) = a \*\ c ) implies f = g )
assume A5: ( ( for a being Element of Z_2
for c being Subset of X holds f . (a,c) = a \*\ c ) & ( for a being Element of Z_2
for c being Subset of X holds g . (a,c) = a \*\ c ) ) ; ::_thesis: f = g
A6: for x being set st x in dom f holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume  x in dom f ; ::_thesis: f . x = g . x
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 = z as Subset of X by A8;
reconsider y = y as Element of Z_2 by A7;
 ( f . (y,z) = y \*\ z & g . (y,z) = y \*\ z ) by A5;
hence  f . x = g . x by A9; ::_thesis: verum
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  f = g by A6, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines bspace-scalar-mult BSPACE:def_6_:_
 for X being set
for b2 being Function of [: the carrier of Z_2,(bool X):],(bool X) holds
( b2 = bspace-scalar-mult X iff for a being Element of Z_2
for c being Subset of X holds b2 . (a,c) = a \*\ c );

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

:: deftheorem  defines bspace BSPACE:def_7_:_
 for X being set holds bspace X = VectSpStr(# (bool X),(bspace-sum X),({} X),(bspace-scalar-mult X) #);

Lm1:  for X being set
for a, b, c being Element of (bspace X)
for 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 X be set ; ::_thesis: for a, b, c being Element of (bspace X)
for 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 )
let a, b, c be Element of (bspace X); ::_thesis: for 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 )
let A, B, C be Subset of X; ::_thesis: ( a = A & b = B & c = C implies ( a + (b + c) = A \+\ (B \+\ C) & (a + b) + c = (A \+\ B) \+\ C ) )
assume that
A1: a = A and
A2: b = B and
A3: c = C ; ::_thesis: ( a + (b + c) = A \+\ (B \+\ C) & (a + b) + c = (A \+\ B) \+\ C )
 b + c = B \+\ C by A2, A3, Def5;
hence  a + (b + c) = A \+\ (B \+\ C) by A1, Def5; ::_thesis: (a + b) + c = (A \+\ B) \+\ C
 a + b = A \+\ B by A1, A2, Def5;
hence  (a + b) + c = (A \+\ B) \+\ C by A3, Def5; ::_thesis: verum
end;

Lm2:  for X being set
for a, b being Element of Z_2
for x, y being Element of (bspace X)
for 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 X be set ; ::_thesis: for a, b being Element of Z_2
for x, y being Element of (bspace X)
for 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) )
let a, b be Element of Z_2; ::_thesis: for x, y being Element of (bspace X)
for 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) )
let x, y be Element of (bspace X); ::_thesis: for 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) )
let c, d be Subset of X; ::_thesis: ( x = c & y = d implies ( (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) ) )
assume that
A1: x = c and
A2: y = d ; ::_thesis: ( (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) )
 ( a * x = a \*\ c & b * y = b \*\ d ) by A1, A2, Def6;
hence  (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) by Def5; ::_thesis: ( a * (x + y) = a \*\ (c \+\ d) & (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )
 x + y = c \+\ d by A1, A2, Def5;
hence  a * (x + y) = a \*\ (c \+\ d) by Def6; ::_thesis: ( (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )
thus  (a + b) * x = (a + b) \*\ c by A1, Def6; ::_thesis: ( (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )
thus  (a * b) * x = (a * b) \*\ c by A1, Def6; ::_thesis: a * (b * x) = a \*\ (b \*\ c)
 b * x = b \*\ c by A1, Def6;
hence  a * (b * x) = a \*\ (b \*\ c) by Def6; ::_thesis: verum
end;

theorem Th21: :: BSPACE:21
for X being set holds bspace X is Abelian
proof
let X be set ; ::_thesis: bspace X is Abelian
let x, y be Element of (bspace X); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
reconsider A = x, B = y as Subset of X ;
x + y = B \+\ A by Def5
.= y + x by Def5 ;
hence  x + y = y + x ; ::_thesis: verum
end;

theorem Th22: :: BSPACE:22
for X being set holds bspace X is add-associative
proof
let X be set ; ::_thesis: bspace X is add-associative
let x, y, z be Element of (bspace X); :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
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  (x + y) + z = x + (y + z) ; ::_thesis: verum
end;

theorem Th23: :: BSPACE:23
for X being set holds bspace X is right_zeroed
proof
let X be set ; ::_thesis: bspace X is right_zeroed
let x be Element of (bspace X); :: according to RLVECT_1:def_4 ::_thesis: x + (0. (bspace X)) = 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  x + (0. (bspace X)) = x ; ::_thesis: verum
end;

theorem Th24: :: BSPACE:24
for X being set holds bspace X is right_complementable
proof
let X be set ; ::_thesis: bspace X is right_complementable
let x be Element of (bspace X); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider A = x as Subset of X ;
take  x ; :: according to ALGSTR_0:def_11 ::_thesis: x + x = 0. (bspace X)
 A \+\ A = {} X by XBOOLE_1:92;
hence  x + x = 0. (bspace X) by Def5; ::_thesis: verum
end;

theorem Th25: :: BSPACE:25
for X being set
for a being Element of Z_2
for x, y being Element of (bspace X) holds a * (x + y) = (a * x) + (a * y)
proof
let X be set ; ::_thesis: for a being Element of Z_2
for x, y being Element of (bspace X) holds a * (x + y) = (a * x) + (a * y)
let a be Element of Z_2; ::_thesis: for x, y being Element of (bspace X) holds a * (x + y) = (a * x) + (a * y)
let x, y be Element of (bspace X); ::_thesis: a * (x + y) = (a * x) + (a * y)
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  a * (x + y) = (a * x) + (a * y) ; ::_thesis: verum
end;

theorem Th26: :: BSPACE:26
for X being set
for a, b being Element of Z_2
for x being Element of (bspace X) holds (a + b) * x = (a * x) + (b * x)
proof
let X be set ; ::_thesis: for a, b being Element of Z_2
for x being Element of (bspace X) holds (a + b) * x = (a * x) + (b * x)
let a, b be Element of Z_2; ::_thesis: for x being Element of (bspace X) holds (a + b) * x = (a * x) + (b * x)
let x be Element of (bspace X); ::_thesis: (a + b) * x = (a * x) + (b * 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  (a + b) * x = (a * x) + (b * x) ; ::_thesis: verum
end;

theorem Th27: :: BSPACE:27
for X being set
for a, b being Element of Z_2
for x being Element of (bspace X) holds (a * b) * x = a * (b * x)
proof
let X be set ; ::_thesis: for a, b being Element of Z_2
for x being Element of (bspace X) holds (a * b) * x = a * (b * x)
let a, b be Element of Z_2; ::_thesis: for x being Element of (bspace X) holds (a * b) * x = a * (b * x)
let x be Element of (bspace X); ::_thesis: (a * b) * x = a * (b * 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  (a * b) * x = a * (b * x) ; ::_thesis: verum
end;

theorem Th28: :: BSPACE:28
for X being set
for x being Element of (bspace X) holds (1_ Z_2) * x = x
proof
let X be set ; ::_thesis: for x being Element of (bspace X) holds (1_ Z_2) * x = x
let x be Element of (bspace X); ::_thesis: (1_ Z_2) * x = x
reconsider c = x as Subset of X ;
(1_ Z_2) * x = (1_ Z_2) \*\ c by Def6
.= c by Def4 ;
hence  (1_ Z_2) * x = x ; ::_thesis: verum
end;

theorem Th29: :: BSPACE:29
for X being set holds
( bspace X is vector-distributive & bspace X is scalar-distributive & bspace X is scalar-associative & bspace X is scalar-unital )
proof
let X be set ; ::_thesis: ( bspace X is vector-distributive & bspace X is scalar-distributive & bspace X is scalar-associative & bspace X is scalar-unital )
thus  bspace X is vector-distributive ::_thesis: ( bspace X is scalar-distributive & bspace X is scalar-associative & bspace X is scalar-unital )
proof
let a be Element of Z_2; :: according to VECTSP_1:def_14 ::_thesis: for b1, b2 being Element of the carrier of (bspace X) holds a * (b1 + b2) = (a * b1) + (a * b2)
let x, y be Element of (bspace X); ::_thesis: a * (x + y) = (a * x) + (a * y)
thus  a * (x + y) = (a * x) + (a * y) by Th25; ::_thesis: verum
end;
thus  bspace X is scalar-distributive ::_thesis: ( bspace X is scalar-associative & bspace X is scalar-unital )
proof
let a, b be Element of Z_2; :: according to VECTSP_1:def_15 ::_thesis: for b1 being Element of the carrier of (bspace X) holds (a + b) * b1 = (a * b1) + (b * b1)
let x be Element of (bspace X); ::_thesis: (a + b) * x = (a * x) + (b * x)
thus  (a + b) * x = (a * x) + (b * x) by Th26; ::_thesis: verum
end;
thus  bspace X is scalar-associative ::_thesis: bspace X is scalar-unital
proof
let a, b be Element of Z_2; :: according to VECTSP_1:def_16 ::_thesis: for b1 being Element of the carrier of (bspace X) holds (a * b) * b1 = a * (b * b1)
let x be Element of (bspace X); ::_thesis: (a * b) * x = a * (b * x)
thus  (a * b) * x = a * (b * x) by Th27; ::_thesis: verum
end;
let x be Element of (bspace X); :: according to VECTSP_1:def_17 ::_thesis: (1. Z_2) * x = x
thus  (1. Z_2) * x = x by Th28; ::_thesis: verum
end;

registration
let X be set ;
cluster bspace X ->  non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ;
coherence
 ( bspace X is vector-distributive & bspace X is scalar-distributive & bspace X is scalar-associative & bspace X is scalar-unital & bspace X is Abelian & bspace X is right_complementable & bspace X is add-associative & bspace X is right_zeroed ) by Th21, Th22, Th23, Th24, Th29;
end;

begin

definition
let X be set ;
func singletons X ->  set  equals :: BSPACE:def 8
 {  f where f is Subset of X : f is 1 -element  }  ;
coherence
  {  f where f is Subset of X : f is 1 -element  }  is set ;
end;

:: deftheorem  defines singletons BSPACE:def_8_:_
 for X being set holds singletons X =  {  f where f is Subset of X : f is 1 -element  }  ;

definition
let X be set ;
:: original: singletons
redefine func singletons X ->  Subset of (bspace X);
coherence
 singletons X is Subset of (bspace X)
proof
set S = singletons X;
 singletons X c= bool X
proof
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in singletons X or f in bool X )
assume  f in singletons X ; ::_thesis: f in bool X
then  ex g being Subset of X st
( f = g & g is 1 -element ) ;
then reconsider f = f as Subset of X ;
 f is Element of bool X ;
hence  f in bool X ; ::_thesis: verum
end;
hence  singletons X is Subset of (bspace X) ; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
cluster singletons X ->  non empty ;
coherence
 not singletons X is empty
proof
set x = the Element of X;
 { the Element of X} in singletons X ;
hence  not singletons X is empty ; ::_thesis: verum
end;
end;

theorem Th30: :: BSPACE:30
for X being non empty set
for f being Subset of X st f is Element of singletons X holds
f is 1 -element
proof
let X be non empty set ; ::_thesis: for f being Subset of X st f is Element of singletons X holds
f is 1 -element
let f be Subset of X; ::_thesis: ( f is Element of singletons X implies f is 1 -element )
assume  f is Element of singletons X ; ::_thesis: f is 1 -element
then  f in singletons X ;
then  ex g being Subset of X st
( g = f & g is 1 -element ) ;
hence  f is 1 -element ; ::_thesis: verum
end;

definition
let F be Field;
let V be VectSp of F;
let l be Linear_Combination of V;
let x be Element of V;
:: original: .
redefine funcl . x ->  Element of F;
coherence
 l . x is Element of F
proof
 l . x in [#] F ;
hence  l . x is Element of F ; ::_thesis: verum
end;
end;

definition
let X be non empty set ;
let s be FinSequence of (bspace X);
let x be Element of X;
funcs @ x ->  FinSequence of Z_2 means :Def9: :: BSPACE:def 9
( len it = len s & ( for j being Nat st 1 <= j & j <= len s holds
it . j = (s . j) @ x ) );
existence
 ex b1 being FinSequence of Z_2 st
( len b1 = len s & ( for j being Nat st 1 <= j & j <= len s holds
b1 . j = (s . j) @ x ) )
proof
deffunc H1( set ) ->  Element of Z_2 = (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 = H1(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; ::_thesis: ( 1 <= j & j <= len s implies p . j = (s . j) @ x )
assume  ( 1 <= j & j <= len s ) ; ::_thesis: p . j = (s . j) @ x
then  j in dom p by A1, FINSEQ_3:25;
hence  p . j = (s . j) @ x by A2; ::_thesis: verum
end;
 rng p c= the carrier of Z_2
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in the carrier of Z_2 )
assume  y in rng p ; ::_thesis: y in the carrier of Z_2
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  y in the carrier of Z_2 by A5; ::_thesis: verum
end;
then reconsider p = p as FinSequence of Z_2 by FINSEQ_1:def_4;
take  p ; ::_thesis: ( len p = len s & ( for j being Nat st 1 <= j & j <= len s holds
p . j = (s . j) @ x ) )
thus  ( len p = len s & ( for j being Nat st 1 <= j & j <= len s holds
p . j = (s . j) @ x ) ) by A1, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of Z_2 st len b1 = len s & ( for j being Nat st 1 <= j & j <= len s holds
b1 . j = (s . j) @ x ) & len b2 = len s & ( for j being Nat st 1 <= j & j <= len s holds
b2 . j = (s . j) @ x ) holds
b1 = b2
proof
let f, g be FinSequence of Z_2; ::_thesis: ( len f = len s & ( for j being Nat st 1 <= j & j <= len s holds
f . j = (s . j) @ x ) & len g = len s & ( for j being Nat st 1 <= j & j <= len s holds
g . j = (s . j) @ x ) implies f = g )
assume 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 ; ::_thesis: f = g
 for k being Nat st 1 <= k & k <= len f holds
f . k = g . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len f implies f . k = g . k )
assume A10: ( 1 <= k & k <= len f ) ; ::_thesis: f . k = g . k
 f . k = (s . k) @ x by A6, A7, A10;
hence  f . k = g . k by A6, A9, A10; ::_thesis: verum
end;
hence  f = g by A6, A8, FINSEQ_1:14; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines @ BSPACE:def_9_:_
 for X being non empty set
for s being FinSequence of (bspace X)
for x being Element of X
for b4 being FinSequence of Z_2 holds
( b4 = s @ x iff ( len b4 = len s & ( for j being Nat st 1 <= j & j <= len s holds
b4 . j = (s . j) @ x ) ) );

theorem Th31: :: BSPACE:31
for X being non empty set
for x being Element of X holds (<*> (bspace X)) @ x = <*> Z_2
proof
let X be non empty set ; ::_thesis: for x being Element of X holds (<*> (bspace X)) @ x = <*> Z_2
let x be Element of X; ::_thesis: (<*> (bspace X)) @ x = <*> Z_2
set V = bspace X;
set L = (<*> (bspace X)) @ x;
len ((<*> (bspace X)) @ x) = len (<*> (bspace X)) by Def9
.= 0 ;
hence  (<*> (bspace X)) @ x = <*> Z_2 ; ::_thesis: verum
end;

theorem Th32: :: BSPACE:32
for X being set
for u, v being Element of (bspace X)
for x being Element of X holds (u + v) @ x = (u @ x) + (v @ x)
proof
let X be set ; ::_thesis: for u, v being Element of (bspace X)
for x being Element of X holds (u + v) @ x = (u @ x) + (v @ x)
let u, v be Element of (bspace X); ::_thesis: for x being Element of X holds (u + v) @ x = (u @ x) + (v @ x)
let x be Element of X; ::_thesis: (u + v) @ x = (u @ x) + (v @ 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  (u + v) @ x = (u @ x) + (v @ x) ; ::_thesis: verum
end;

theorem Th33: :: BSPACE:33
for X being non empty set
for s being FinSequence of (bspace X)
for f being Element of (bspace X)
for x being Element of X holds (s ^ <*f*>) @ x = (s @ x) ^ <*(f @ x)*>
proof
let X be non empty set ; ::_thesis: for s being FinSequence of (bspace X)
for f being Element of (bspace X)
for x being Element of X holds (s ^ <*f*>) @ x = (s @ x) ^ <*(f @ x)*>
let s be FinSequence of (bspace X); ::_thesis: for f being Element of (bspace X)
for x being Element of X holds (s ^ <*f*>) @ x = (s @ x) ^ <*(f @ x)*>
let f be Element of (bspace X); ::_thesis: for x being Element of X holds (s ^ <*f*>) @ x = (s @ x) ^ <*(f @ x)*>
let x be Element of X; ::_thesis: (s ^ <*f*>) @ x = (s @ x) ^ <*(f @ x)*>
set L = (s ^ <*f*>) @ x;
set R = (s @ x) ^ <*(f @ x)*>;
A1: len ((s ^ <*f*>) @ x) = 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 ((s ^ <*f*>) @ x) holds
((s ^ <*f*>) @ x) . k = ((s @ x) ^ <*(f @ x)*>) . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len ((s ^ <*f*>) @ x) implies ((s ^ <*f*>) @ x) . k = ((s @ x) ^ <*(f @ x)*>) . k )
assume that
A3: 1 <= k and
A4: k <= len ((s ^ <*f*>) @ x) ; ::_thesis: ((s ^ <*f*>) @ x) . k = ((s @ x) ^ <*(f @ x)*>) . k
A5: k in NAT by ORDINAL1:def_12;
percases ( k <= len s or k = len ((s ^ <*f*>) @ x) ) by A1, A4, NAT_1:8;
supposeA6: k <= len s ; ::_thesis: ((s ^ <*f*>) @ x) . k = ((s @ x) ^ <*(f @ x)*>) . k
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: ((s @ x) ^ <*(f @ x)*>) . 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  ((s ^ <*f*>) @ x) . k = ((s ^ <*f*>) . k) @ x by A3, Def9;
hence  ((s ^ <*f*>) @ x) . k = ((s @ x) ^ <*(f @ x)*>) . k by A7, A8, FINSEQ_1:def_7; ::_thesis: verum
end;
supposeA9: k = len ((s ^ <*f*>) @ x) ; ::_thesis: ((s ^ <*f*>) @ x) . k = ((s @ x) ^ <*(f @ x)*>) . k
 dom <*(f @ x)*> = {1} by FINSEQ_1:2, FINSEQ_1:def_8;
then A10: 1 in dom <*(f @ x)*> by TARSKI:def_1;
 len (s @ x) = len s by Def9;
then A11: ((s @ x) ^ <*(f @ x)*>) . 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, FINSEQ_1: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  ((s ^ <*f*>) @ x) . k = ((s @ x) ^ <*(f @ x)*>) . k by A3, A11, A12, Def9; ::_thesis: verum
end;
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  (s ^ <*f*>) @ x = (s @ x) ^ <*(f @ x)*> by A1, A2, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th34: :: BSPACE:34
for X being non empty set
for s being FinSequence of (bspace X)
for x being Element of X holds (Sum s) @ x = Sum (s @ x)
proof
let X be non empty set ; ::_thesis: for s being FinSequence of (bspace X)
for x being Element of X holds (Sum s) @ x = Sum (s @ x)
let s be FinSequence of (bspace X); ::_thesis: for x being Element of X holds (Sum s) @ x = Sum (s @ x)
let x be Element of X; ::_thesis: (Sum s) @ x = Sum (s @ x)
set V = bspace X;
defpred S1[ FinSequence of (bspace X)] means (Sum $1) @ x = Sum ($1 @ x);
A1: S1[ <*> (bspace X)]
proof
reconsider z = 0. (bspace X) as Subset of X ;
set e = <*> (bspace X);
A2: z @ x = 0. Z_2 by Def3;
 ( Sum (<*> (bspace X)) = 0. (bspace X) & (<*> (bspace X)) @ x = <*> Z_2 ) by Th31, RLVECT_1:43;
hence  S1[ <*> (bspace X)] by A2, RLVECT_1:43; ::_thesis: verum
end;
A3: for p being FinSequence of (bspace X)
for f being Element of (bspace X) st S1[p] holds
S1[p ^ <*f*>]
proof
let p be FinSequence of (bspace X); ::_thesis: for f being Element of (bspace X) st S1[p] holds
S1[p ^ <*f*>]
let f be Element of (bspace X); ::_thesis: ( S1[p] implies S1[p ^ <*f*>] )
assume A4: S1[p] ; ::_thesis: S1[p ^ <*f*>]
(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  S1[p ^ <*f*>] ; ::_thesis: verum
end;
 for p being FinSequence of (bspace X) holds S1[p] from BSPACE:sch_1(A1, A3);
hence  (Sum s) @ x = Sum (s @ x) ; ::_thesis: verum
end;

theorem Th35: :: BSPACE:35
for X being non empty set
for l being Linear_Combination of bspace X
for x being Element of (bspace X) st x in Carrier l holds
l . x = 1_ Z_2
proof
let X be non empty set ; ::_thesis: for l being Linear_Combination of bspace X
for x being Element of (bspace X) st x in Carrier l holds
l . x = 1_ Z_2
let l be Linear_Combination of bspace X; ::_thesis: for x being Element of (bspace X) st x in Carrier l holds
l . x = 1_ Z_2
let x be Element of (bspace X); ::_thesis: ( x in Carrier l implies l . x = 1_ Z_2 )
assume  x in Carrier l ; ::_thesis: l . x = 1_ Z_2
then  l . x <> 0. Z_2 by VECTSP_6:2;
hence  l . x = 1_ Z_2 by Th5, Th6, CARD_1:50, TARSKI:def_2; ::_thesis: verum
end;

registration
let X be empty set ;
cluster singletons X ->  empty ;
coherence
 singletons X is empty
proof
assume  not singletons X is empty ; ::_thesis: contradiction
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  contradiction ; ::_thesis: verum
end;
end;

theorem Th36: :: BSPACE:36
for X being set holds singletons X is linearly-independent
proof
let X be set ; ::_thesis: singletons X is linearly-independent
percases ( X is empty or not X is empty ) ;
suppose X is empty ; ::_thesis: singletons X is linearly-independent
hence  singletons X is linearly-independent ; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: singletons X is linearly-independent
then reconsider X = X as non empty set ;
set V = bspace X;
set S = singletons X;
 for l being Linear_Combination of singletons X st Sum l = 0. (bspace X) holds
Carrier l = {}
proof
let l be Linear_Combination of singletons X; ::_thesis: ( Sum l = 0. (bspace X) implies Carrier l = {} )
assume A1: Sum l = 0. (bspace X) ; ::_thesis: Carrier l = {}
reconsider s = Sum l as Subset of X ;
set C = Carrier l;
A2: l ! (Carrier l) = l by RANKNULL:24;
assume  Carrier l <> {} ; ::_thesis: contradiction
then consider f being Element of (bspace X) such that
A3: f in Carrier l by SUBSET_1:4;
reconsider f = f as Subset of X ;
reconsider g = f as Element of (bspace X) ;
A4: {g} c= Carrier l by A3, ZFMISC_1:31;
reconsider n = l ! {g} as Linear_Combination of {g} ;
reconsider m = l ! ((Carrier l) \ {g}) as Linear_Combination of (Carrier l) \ {g} ;
reconsider l = l as Linear_Combination of Carrier l 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;
 Carrier l c= singletons X 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 Carrier l holds
g @ x = 0. Z_2
proof
let g be Subset of X; ::_thesis: ( g <> f & g in Carrier l implies g @ x = 0. Z_2 )
assume that
A10: g <> f and
A11: g in Carrier l ; ::_thesis: g @ x = 0. Z_2
 Carrier l c= singletons X 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__::_thesis:_not_g_@_x_<>_0._Z_2
assume  g @ x <> 0. Z_2 ; ::_thesis: contradiction
then  x in {y} by A12, Def3;
hence  contradiction by A7, A10, A12, TARSKI:def_1; ::_thesis: verum
end;
hence  g @ x = 0. Z_2 ; ::_thesis: verum
end;
A13: t @ x = 0
proof
consider F being FinSequence of (bspace X) 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 (bspace X) 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 (bspace X); ::_thesis: ( F is one-to-one & rng F = Carrier m implies (m (#) F) @ x = (len F) |-> (0. Z_2) )
assume that
 F is one-to-one and
A17: rng F = Carrier m ; ::_thesis: (m (#) F) @ x = (len F) |-> (0. Z_2)
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 ((m (#) F) @ x) = len F by Def9;
A20: for k being Nat st 1 <= k & k <= len ((m (#) F) @ x) holds
((m (#) F) @ x) . k = ((len F) |-> (0. Z_2)) . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len ((m (#) F) @ x) implies ((m (#) F) @ x) . k = ((len F) |-> (0. Z_2)) . k )
assume A21: ( 1 <= k & k <= len ((m (#) F) @ x) ) ; ::_thesis: ((m (#) F) @ x) . k = ((len F) |-> (0. Z_2)) . k
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= (Carrier l) \ {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 Carrier l by A25, XBOOLE_0:def_5;
A31: Fk <> f
proof
assume  Fk = f ; ::_thesis: contradiction
then  not f in {f} by A29, A25, XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
((m (#) F) @ x) . k = ((m (#) F) . k) @ x by A18, A19, A21, Def9
.= 0. Z_2 by A9, A28, A31, A30 ;
hence  ((m (#) F) @ x) . k = ((len F) |-> (0. Z_2)) . k by A23, FUNCOP_1:7; ::_thesis: verum
end;
 dom ((len F) |-> (0. Z_2)) = Seg (len F) by FUNCOP_1:13;
then  len ((m (#) F) @ x) = len ((len F) |-> (0. Z_2)) by A19, FINSEQ_1:def_3;
hence  (m (#) F) @ x = (len F) |-> (0. Z_2) by A20, FINSEQ_1:14; ::_thesis: verum
end;
then  (m (#) F) @ x = (len F) |-> (0. Z_2) by A14;
hence  t @ x = 0 by A15, A16, Th5, MATRIX_3:11; ::_thesis: verum
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  contradiction by A8, A32, A13, A6, Th5, RLVECT_1:4; ::_thesis: verum
end;
hence  singletons X is linearly-independent by VECTSP_7:def_1; ::_thesis: verum
end;
end;
end;

theorem :: BSPACE:37
for X being set
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: :: BSPACE:38
for X being finite set
for A being Subset of X ex l being Linear_Combination of singletons X st Sum l = A
proof
let X be finite set ; ::_thesis: for A being Subset of X ex l being Linear_Combination of singletons X st Sum l = A
let A be Subset of X; ::_thesis: ex l being Linear_Combination of singletons X st Sum l = A
set V = bspace X;
set S = singletons X;
defpred S1[ set ] means ( $1 is Subset of X implies ex l being Linear_Combination of singletons X st Sum l = $1 );
A1: S1[ {} ]
proof
reconsider l = ZeroLC (bspace X) as Linear_Combination of singletons X by VECTSP_6:5;
assume  {} is Subset of X ; ::_thesis: ex l being Linear_Combination of singletons X st Sum l = {}
take  l ; ::_thesis: Sum l = {}
 Sum l = 0. (bspace X) by VECTSP_6:15;
hence  Sum l = {} ; ::_thesis: verum
end;
A2: for x, B being set st x in A & B c= A & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; ::_thesis: ( x in A & B c= A & S1[B] implies S1[B \/ {x}] )
assume that
 x in A and
 B c= A and
A3: S1[B] ; ::_thesis: S1[B \/ {x}]
assume A4: B \/ {x} is Subset of X ; ::_thesis: ex l being Linear_Combination of singletons X st Sum l = B \/ {x}
then reconsider B = B as Subset of X by XBOOLE_1:11;
consider l being Linear_Combination of singletons X such that
A5: Sum l = B by A3;
percases ( x in B or not x in B ) ;
supposeA6: x in B ; ::_thesis: ex l being Linear_Combination of singletons X st Sum l = B \/ {x}
take  l ; ::_thesis: Sum l = B \/ {x}
thus  Sum l = B \/ {x} by A5, A6, ZFMISC_1:40; ::_thesis: verum
end;
suppose not x in B ; ::_thesis: ex l being Linear_Combination of singletons X st Sum l = B \/ {x}
then A7: B misses {x} by ZFMISC_1:50;
reconsider z = ZeroLC (bspace X) as Linear_Combination of {} (bspace X) by VECTSP_6:5;
reconsider f = {x} as Element of (bspace X) by A4, XBOOLE_1:11;
reconsider g = f as Subset of X ;
set m = z +* (f,(1_ Z_2));
 z +* (f,(1_ Z_2)) is Linear_Combination of ({} (bspace X)) \/ {f} by RANKNULL:23;
then reconsider m = z +* (f,(1_ Z_2)) as Linear_Combination of {f} ;
 dom z = [#] (bspace X) by FUNCT_2:92;
then A8: m . f = 1_ Z_2 by FUNCT_7:31;
 f in singletons X ;
then  {f} c= singletons X by ZFMISC_1:31;
then  m is Linear_Combination of singletons X by VECTSP_6:4;
then reconsider n = l + m as Linear_Combination of singletons X by VECTSP_6:24;
take  n ; ::_thesis: Sum n = B \/ {x}
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  Sum n = B \/ {x} ; ::_thesis: verum
end;
end;
end;
A9: A is finite ;
 S1[A] from FINSET_1:sch_2(A9, A1, A2);
hence  ex l being Linear_Combination of singletons X st Sum l = A ; ::_thesis: verum
end;

theorem Th39: :: BSPACE:39
for X being finite set holds Lin (singletons X) = bspace X
proof
let X be finite set ; ::_thesis: Lin (singletons X) = bspace X
set V = bspace X;
set S = singletons X;
 for v being Element of (bspace X) holds v in Lin (singletons X)
proof
let v be Element of (bspace X); ::_thesis: v in Lin (singletons X)
reconsider f = v as Subset of X ;
consider A being set  such that
A1: A c= X and
A2: f = A ;
reconsider A = A as Subset of X by A1;
 ex l being Linear_Combination of singletons X st Sum l = A by Th38;
hence  v in Lin (singletons X) by A2, VECTSP_7:7; ::_thesis: verum
end;
hence  Lin (singletons X) = bspace X by VECTSP_4:32; ::_thesis: verum
end;

theorem Th40: :: BSPACE:40
for X being finite set holds singletons X is Basis of bspace X
proof
let X be finite set ; ::_thesis: singletons X is Basis of bspace X
 ( singletons X is linearly-independent & Lin (singletons X) = bspace X ) by Th36, Th39;
hence  singletons X is Basis of bspace X by VECTSP_7:def_3; ::_thesis: verum
end;

registration
let X be finite set ;
cluster singletons X ->  finite ;
coherence
 singletons X is finite ;
end;

registration
let X be finite set ;
cluster bspace X ->  non empty finite-dimensional ;
coherence
 bspace X is finite-dimensional
proof
set S = singletons X;
 singletons X is Basis of bspace X by Th40;
hence  bspace X is finite-dimensional by MATRLIN:def_1; ::_thesis: verum
end;
end;

theorem :: BSPACE:41
for X being set holds card (singletons X) = card X
proof
let X be set ; ::_thesis: card (singletons X) = card X
defpred S1[ set , set ] means ( $1 in X & $2 = {$1} );
A1: for x being set st x in X holds
ex y being set st S1[x,y] ;
consider f being Function such that
A2: dom f = X and
A3: for x being set st x in X holds
S1[x,f . x] from CLASSES1:sch_1(A1);
A4: rng f = singletons X
proof
thus  rng f c= singletons X :: according to XBOOLE_0:def_10 ::_thesis: singletons X c= rng f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in singletons X )
assume  y in rng f ; ::_thesis: y in singletons X
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  y in singletons X by A6; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in singletons X or y in rng f )
assume A8: y in singletons X ; ::_thesis: y in rng f
reconsider X = 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 = 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  y in rng f by A2, FUNCT_1:3; ::_thesis: verum
end;
 f is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A10: ( x1 in dom f & x2 in dom f ) and
A11: f . x1 = f . x2 ; ::_thesis: x1 = x2
 ( S1[x1,f . x1] & S1[x2,f . x2] ) by A2, A3, A10;
hence  x1 = x2 by A11, ZFMISC_1:3; ::_thesis: verum
end;
then  X, singletons X are_equipotent by A2, A4, WELLORD2:def_4;
hence  card (singletons X) = card X by CARD_1:5; ::_thesis: verum
end;

theorem :: BSPACE:42
for X being set holds 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  dim (bspace {}) = 0 by RANKNULL:5; ::_thesis: verum
end;