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

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

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

j in dom A
by A3, A7, FINSEQ_1:def 3;
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 )

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;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
i <> j
; :: thesis: x . i = 0. Z_2
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;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

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

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