let n be non zero Element of NAT ; :: thesis: for A being FinSequence of n -tuples_on BOOLEAN
for B being finite Subset of ()
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 ()
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 (); :: 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 S1[ 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 & S1[x,y] )
proof
let x be object ; :: thesis: ( x in B implies ex y being object st
( y in the carrier of Z_2 & S1[x,y] ) )

assume A5: x in B ; :: thesis: ex y being object st
( y in the carrier of Z_2 & S1[x,y] )

consider j being object such that
A6: ( j in dom A & x = A . j ) by ;
A7: j in Seg n by ;
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 & S1[x,y] ) by A6, A7; :: thesis: verum
end;
consider l0 being Function of B, the carrier of Z_2 such that
A8: for x being object st x in B holds
S1[x,l0 . x] from A9: for j being Nat st j in Seg n holds
l0 . (A . j) = v . j
proof
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 ;
then consider i being Nat such that
A11: ( i in Seg n & A . j = A . i & l0 . (A . j) = v . i ) by ;
i in dom A by ;
hence l0 . (A . j) = v . j by ; :: thesis: verum
end;
set f = the carrier of () --> ();
set l = ( the carrier of () --> ()) +* l0;
A12: dom (( the carrier of () --> ()) +* l0) = (dom ( the carrier of () --> ())) \/ (dom l0) by FUNCT_4:def 1
.= the carrier of () \/ (dom l0)
.= the carrier of () \/ B by FUNCT_2:def 1
.= the carrier of () by XBOOLE_1:12 ;
rng (( the carrier of () --> ()) +* l0) c= the carrier of Z_2 ;
then ( the carrier of () --> ()) +* l0 is Function of the carrier of (), the carrier of Z_2 by ;
then reconsider l = ( the carrier of () --> ()) +* l0 as Element of Funcs ( the carrier of (), the carrier of Z_2) by FUNCT_2:8;
A13: for v being Element of () st not v in B holds
l . v = 0. Z_2
proof
let v be Element of (); :: 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 () --> ())) \/ (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 () --> ()) . v by ;
hence l . v = 0. Z_2 ; :: thesis: verum
end;
then reconsider l = l as Linear_Combination of n -BinaryVectSp by VECTSP_6:def 1;
for x being object st x in Carrier l holds
x in B
proof
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 () st
( x = v & l . v <> 0. Z_2 ) ;
hence x in B by A13; :: thesis: verum
end;
then A15: l is Linear_Combination of B by ;
for j being Nat st j in Seg n holds
v . j = l . (A . j)
proof
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 ;
then A17: A . j in B by ;
then reconsider x = A . j as Element of () ;
A18: x in dom l0 by ;
x in dom l by A12;
then A19: x in (dom ( the carrier of () --> ())) \/ (dom l0) by FUNCT_4:def 1;
thus l . (A . j) = l0 . x by
.= v . j by ; :: thesis: verum
end;
hence ex l being Linear_Combination of B st
for j being Nat st j in Seg n holds
v . j = l . (A . j) by A15; :: thesis: verum