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 ()
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 ()
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 (); :: 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 () ;
A8: j in Seg n by ;
A9: Carrier l c= rng FA by ;
A10: len (l (#) FA) = m by ;
Suml = Sum (l (#) FA) by ;
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 ;
A16: i in dom (l (#) FA) by ;
A17: K = (l . (FA /. i)) * (FA /. i) by ;
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 ;
A19: i in dom A by ;
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 ; :: 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 ; :: thesis: verum
end;
j in dom A by ;
then l . (A . j) is Element of Z_2 by ;
hence Suml . j = l . (A . j) by Th5, A7, A11, A12; :: thesis: verum