let m, 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 l being Linear_Combination of B
for Suml being Element of n -tuples_on BOOLEAN st rng A = B & m <= n & len A = m & Suml = Sum l & A is one-to-one & ( for i, j being Nat st i in Seg n & j in Seg m holds
( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) holds
for j being Nat st j in Seg m holds
Suml . j = l . (A . j)
let A be FinSequence of n -tuples_on BOOLEAN; :: thesis: for B being finite Subset of (n -BinaryVectSp)
for l being Linear_Combination of B
for Suml being Element of n -tuples_on BOOLEAN st rng A = B & m <= n & len A = m & Suml = Sum l & A is one-to-one & ( for i, j being Nat st i in Seg n & j in Seg m holds
( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) holds
for j being Nat st j in Seg m holds
Suml . j = l . (A . j)
let B be finite Subset of (n -BinaryVectSp); :: thesis: for l being Linear_Combination of B
for Suml being Element of n -tuples_on BOOLEAN st rng A = B & m <= n & len A = m & Suml = Sum l & A is one-to-one & ( for i, j being Nat st i in Seg n & j in Seg m holds
( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) holds
for j being Nat st j in Seg m holds
Suml . j = l . (A . j)
let l be Linear_Combination of B; :: thesis: for Suml being Element of n -tuples_on BOOLEAN st rng A = B & m <= n & len A = m & Suml = Sum l & A is one-to-one & ( for i, j being Nat st i in Seg n & j in Seg m holds
( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) holds
for j being Nat st j in Seg m holds
Suml . j = l . (A . j)
let Suml be Element of n -tuples_on BOOLEAN; :: thesis: ( rng A = B & m <= n & len A = m & Suml = Sum l & A is one-to-one & ( for i, j being Nat st i in Seg n & j in Seg m holds
( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) implies for j being Nat st j in Seg m holds
Suml . j = l . (A . j) )
assume that
A1: rng A = B and
A2: m <= n and
A3: len A = m and
A4: Suml = Sum l and
A5: A is one-to-one and
A6: for i, j being Nat st i in Seg n & j in Seg m holds
( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ; :: thesis: for j being Nat st j in Seg m holds
Suml . j = l . (A . j)
set V = n -BinaryVectSp ;
let j be Nat; :: thesis: ( j in Seg m implies Suml . j = l . (A . j) )
assume A7: j in Seg m ; :: thesis: Suml . j = l . (A . j)
reconsider FA = A as FinSequence of (n -BinaryVectSp) ;
A8: j in Seg n by A7, A2, FINSEQ_1:5, TARSKI:def 3;
A9: Carrier l c= rng FA by A1, VECTSP_6:def 4;
A10: len (l (#) FA) = m by A3, VECTSP_6:def 5;
Suml = Sum (l (#) FA) by VECTSP_9:3, A5, A9, A4;
then consider x being FinSequence of Z_2 such that
A11: ( len x = m & Suml . j = Sum x & ( for i being Nat st i in Seg m holds
ex K being Element of n -tuples_on BOOLEAN st
( K = (l (#) FA) . i & x . i = K . j ) ) ) by Th7, A2, A8, A10;
A12: for i being Nat st i in Seg m holds
( ( i = j implies x . i = l . (A . j) ) & ( i <> j implies x . i = 0. Z_2 ) )

proof

let i be Nat; :: thesis: ( i in Seg m implies ( ( i = j implies x . i = l . (A . j) ) & ( i <> j implies x . i = 0. Z_2 ) ) )
assume A13: i in Seg m ; :: thesis: ( ( i = j implies x . i = l . (A . j) ) & ( i <> j implies x . i = 0. Z_2 ) )
then consider K being Element of n -tuples_on BOOLEAN such that
A14: ( K = (l (#) FA) . i & x . i = K . j ) by A11;
A15: i in Seg n by A13, A2, FINSEQ_1:5, TARSKI:def 3;
A16: i in dom (l (#) FA) by FINSEQ_1:def 3, A13, A10;
A17: K = (l . (FA /. i)) * (FA /. i) by A14, A16, VECTSP_6:def 5;
reconsider FAi = FA /. i as Element of n -tuples_on BOOLEAN ;
set lFAi = l . (FA /. i);
A18: K . j = (l . (FA /. i)) '&' (FAi . j) by Def4, A8, A17, BSPACE:3;
A19: i in dom A by A3, FINSEQ_1:def 3, A13;
then A20: FAi . j = (A . i) . j by PARTFUN1:def 6;
thus ( i = j implies x . i = l . (A . j) ) :: thesis: ( i <> j implies x . i = 0. Z_2 )

proof

assume A21: i = j ; :: thesis: x . i = l . (A . j)
then K . j = (l . (FA /. i)) '&' TRUE by A6, A8, A13, A18, A20;
hence x . i = l . (A . j) by A21, A14, A19, PARTFUN1:def 6; :: thesis: verum

end;

assume i <> j ; :: thesis: x . i = 0. Z_2
then K . j = (l . (FA /. i)) '&' FALSE by A6, A7, A15, A18, A20;
hence x . i = 0. Z_2 by A14, BSPACE:5; :: thesis: verum

end;

j in dom A by A3, A7, FINSEQ_1:def 3;
then l . (A . j) is Element of Z_2 by PARTFUN1:4, FUNCT_2:5;
hence Suml . j = l . (A . j) by Th5, A7, A11, A12; :: thesis: verum