let n be non zero Element of NAT ; :: thesis: for A being FinSequence of n -tuples_on BOOLEAN

for B being finite Subset of (n -BinaryVectSp)

for v being Element of n -tuples_on BOOLEAN st rng A = B & len A = n & A is one-to-one holds

ex l being Linear_Combination of B st

for j being Nat st j in Seg n holds

v . j = l . (A . j)

let A be FinSequence of n -tuples_on BOOLEAN; :: thesis: for B being finite Subset of (n -BinaryVectSp)

for v being Element of n -tuples_on BOOLEAN st rng A = B & len A = n & A is one-to-one holds

ex l being Linear_Combination of B st

for j being Nat st j in Seg n holds

v . j = l . (A . j)

let B be finite Subset of (n -BinaryVectSp); :: thesis: for v being Element of n -tuples_on BOOLEAN st rng A = B & len A = n & A is one-to-one holds

ex l being Linear_Combination of B st

for j being Nat st j in Seg n holds

v . j = l . (A . j)

let v be Element of n -tuples_on BOOLEAN; :: thesis: ( rng A = B & len A = n & A is one-to-one implies ex l being Linear_Combination of B st

for j being Nat st j in Seg n holds

v . j = l . (A . j) )

assume that

A1: rng A = B and

A2: len A = n and

A3: A is one-to-one ; :: thesis: ex l being Linear_Combination of B st

for j being Nat st j in Seg n holds

v . j = l . (A . j)

set V = n -BinaryVectSp ;

defpred S_{1}[ object , object ] means ex j being Nat st

( j in Seg n & $1 = A . j & $2 = v . j );

A4: for x being object st x in B holds

ex y being object st

( y in the carrier of Z_2 & S_{1}[x,y] )

A8: for x being object st x in B holds

S_{1}[x,l0 . x]
from FUNCT_2:sch 1(A4);

A9: for j being Nat st j in Seg n holds

l0 . (A . j) = v . j

set l = ( the carrier of (n -BinaryVectSp) --> (0. Z_2)) +* l0;

A12: dom (( the carrier of (n -BinaryVectSp) --> (0. Z_2)) +* l0) = (dom ( the carrier of (n -BinaryVectSp) --> (0. Z_2))) \/ (dom l0) by FUNCT_4:def 1

.= the carrier of (n -BinaryVectSp) \/ (dom l0)

.= the carrier of (n -BinaryVectSp) \/ B by FUNCT_2:def 1

.= the carrier of (n -BinaryVectSp) by XBOOLE_1:12 ;

rng (( the carrier of (n -BinaryVectSp) --> (0. Z_2)) +* l0) c= the carrier of Z_2 ;

then ( the carrier of (n -BinaryVectSp) --> (0. Z_2)) +* l0 is Function of the carrier of (n -BinaryVectSp), the carrier of Z_2 by FUNCT_2:2, A12;

then reconsider l = ( the carrier of (n -BinaryVectSp) --> (0. Z_2)) +* l0 as Element of Funcs ( the carrier of (n -BinaryVectSp), the carrier of Z_2) by FUNCT_2:8;

A13: for v being Element of (n -BinaryVectSp) st not v in B holds

l . v = 0. Z_2

for x being object st x in Carrier l holds

x in B

for j being Nat st j in Seg n holds

v . j = l . (A . j)

for j being Nat st j in Seg n holds

v . j = l . (A . j) by A15; :: thesis: verum

for B being finite Subset of (n -BinaryVectSp)

for v being Element of n -tuples_on BOOLEAN st rng A = B & len A = n & A is one-to-one holds

ex l being Linear_Combination of B st

for j being Nat st j in Seg n holds

v . j = l . (A . j)

let A be FinSequence of n -tuples_on BOOLEAN; :: thesis: for B being finite Subset of (n -BinaryVectSp)

for v being Element of n -tuples_on BOOLEAN st rng A = B & len A = n & A is one-to-one holds

ex l being Linear_Combination of B st

for j being Nat st j in Seg n holds

v . j = l . (A . j)

let B be finite Subset of (n -BinaryVectSp); :: thesis: for v being Element of n -tuples_on BOOLEAN st rng A = B & len A = n & A is one-to-one holds

ex l being Linear_Combination of B st

for j being Nat st j in Seg n holds

v . j = l . (A . j)

let v be Element of n -tuples_on BOOLEAN; :: thesis: ( rng A = B & len A = n & A is one-to-one implies ex l being Linear_Combination of B st

for j being Nat st j in Seg n holds

v . j = l . (A . j) )

assume that

A1: rng A = B and

A2: len A = n and

A3: A is one-to-one ; :: thesis: ex l being Linear_Combination of B st

for j being Nat st j in Seg n holds

v . j = l . (A . j)

set V = n -BinaryVectSp ;

defpred S

( j in Seg n & $1 = A . j & $2 = v . j );

A4: for x being object st x in B holds

ex y being object st

( y in the carrier of Z_2 & S

proof

consider l0 being Function of B, the carrier of Z_2 such that
let x be object ; :: thesis: ( x in B implies ex y being object st

( y in the carrier of Z_2 & S_{1}[x,y] ) )

assume A5: x in B ; :: thesis: ex y being object st

( y in the carrier of Z_2 & S_{1}[x,y] )

consider j being object such that

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

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

reconsider j = j as Nat by A6;

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

hence ex y being object st

( y in the carrier of Z_2 & S_{1}[x,y] )
by A6, A7; :: thesis: verum

end;( y in the carrier of Z_2 & S

assume A5: x in B ; :: thesis: ex y being object st

( y in the carrier of Z_2 & S

consider j being object such that

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

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

reconsider j = j as Nat by A6;

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

hence ex y being object st

( y in the carrier of Z_2 & S

A8: for x being object st x in B holds

S

A9: for j being Nat st j in Seg n holds

l0 . (A . j) = v . j

proof

set f = the carrier of (n -BinaryVectSp) --> (0. Z_2);
let j be Nat; :: thesis: ( j in Seg n implies l0 . (A . j) = v . j )

assume j in Seg n ; :: thesis: l0 . (A . j) = v . j

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

then consider i being Nat such that

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

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

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

end;assume j in Seg n ; :: thesis: l0 . (A . j) = v . j

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

then consider i being Nat such that

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

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

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

set l = ( the carrier of (n -BinaryVectSp) --> (0. Z_2)) +* l0;

A12: dom (( the carrier of (n -BinaryVectSp) --> (0. Z_2)) +* l0) = (dom ( the carrier of (n -BinaryVectSp) --> (0. Z_2))) \/ (dom l0) by FUNCT_4:def 1

.= the carrier of (n -BinaryVectSp) \/ (dom l0)

.= the carrier of (n -BinaryVectSp) \/ B by FUNCT_2:def 1

.= the carrier of (n -BinaryVectSp) by XBOOLE_1:12 ;

rng (( the carrier of (n -BinaryVectSp) --> (0. Z_2)) +* l0) c= the carrier of Z_2 ;

then ( the carrier of (n -BinaryVectSp) --> (0. Z_2)) +* l0 is Function of the carrier of (n -BinaryVectSp), the carrier of Z_2 by FUNCT_2:2, A12;

then reconsider l = ( the carrier of (n -BinaryVectSp) --> (0. Z_2)) +* l0 as Element of Funcs ( the carrier of (n -BinaryVectSp), the carrier of Z_2) by FUNCT_2:8;

A13: for v being Element of (n -BinaryVectSp) st not v in B holds

l . v = 0. Z_2

proof

then reconsider l = l as Linear_Combination of n -BinaryVectSp by VECTSP_6:def 1;
let v be Element of (n -BinaryVectSp); :: thesis: ( not v in B implies l . v = 0. Z_2 )

v in dom l by A12;

then A14: v in (dom ( the carrier of (n -BinaryVectSp) --> (0. Z_2))) \/ (dom l0) by FUNCT_4:def 1;

assume not v in B ; :: thesis: l . v = 0. Z_2

then not v in dom l0 ;

then l . v = ( the carrier of (n -BinaryVectSp) --> (0. Z_2)) . v by A14, FUNCT_4:def 1;

hence l . v = 0. Z_2 ; :: thesis: verum

end;v in dom l by A12;

then A14: v in (dom ( the carrier of (n -BinaryVectSp) --> (0. Z_2))) \/ (dom l0) by FUNCT_4:def 1;

assume not v in B ; :: thesis: l . v = 0. Z_2

then not v in dom l0 ;

then l . v = ( the carrier of (n -BinaryVectSp) --> (0. Z_2)) . v by A14, FUNCT_4:def 1;

hence l . v = 0. Z_2 ; :: thesis: verum

for x being object st x in Carrier l holds

x in B

proof

then A15:
l is Linear_Combination of B
by TARSKI:def 3, VECTSP_6:def 4;
let x be object ; :: thesis: ( x in Carrier l implies x in B )

assume x in Carrier l ; :: thesis: x in B

then ex v being Element of (n -BinaryVectSp) st

( x = v & l . v <> 0. Z_2 ) ;

hence x in B by A13; :: thesis: verum

end;assume x in Carrier l ; :: thesis: x in B

then ex v being Element of (n -BinaryVectSp) st

( x = v & l . v <> 0. Z_2 ) ;

hence x in B by A13; :: thesis: verum

for j being Nat st j in Seg n holds

v . j = l . (A . j)

proof

hence
ex l being Linear_Combination of B st
let j be Nat; :: thesis: ( j in Seg n implies v . j = l . (A . j) )

assume A16: j in Seg n ; :: thesis: v . j = l . (A . j)

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

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

then reconsider x = A . j as Element of (n -BinaryVectSp) ;

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

x in dom l by A12;

then A19: x in (dom ( the carrier of (n -BinaryVectSp) --> (0. Z_2))) \/ (dom l0) by FUNCT_4:def 1;

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

.= v . j by A9, A16 ; :: thesis: verum

end;assume A16: j in Seg n ; :: thesis: v . j = l . (A . j)

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

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

then reconsider x = A . j as Element of (n -BinaryVectSp) ;

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

x in dom l by A12;

then A19: x in (dom ( the carrier of (n -BinaryVectSp) --> (0. Z_2))) \/ (dom l0) by FUNCT_4:def 1;

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

.= v . j by A9, A16 ; :: thesis: verum

for j being Nat st j in Seg n holds

v . j = l . (A . j) by A15; :: thesis: verum