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₁[ 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₁[x,y] )

proof

let x be object ; :: thesis: ( x in B implies ex y being object st
( y in the carrier of Z_2 & S₁[x,y] ) )
assume A5: x in B ; :: thesis: ex y being object st
( y in the carrier of Z_2 & S₁[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₁[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
S₁[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

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 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;

set f = the carrier of (n -BinaryVectSp) --> (0. Z_2);
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

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;

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 (n -BinaryVectSp) 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 TARSKI:def 3, VECTSP_6:def 4;
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 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;

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