let m be non zero Element of NAT ; :: thesis: for x being FinSequence of Z_2

for v being Element of Z_2

for j being Nat st len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) holds

Sum x = v

defpred S_{1}[ Nat] means for m being non zero Element of NAT

for x being FinSequence of Z_2

for v being Element of Z_2

for j being Nat st $1 = m & len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) holds

Sum x = v;

A1: S_{1}[ 0 ]
;

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A1, A2);

hence for x being FinSequence of Z_2

for v being Element of Z_2

for j being Nat st len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) holds

Sum x = v ; :: thesis: verum

for v being Element of Z_2

for j being Nat st len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) holds

Sum x = v

defpred S

for x being FinSequence of Z_2

for v being Element of Z_2

for j being Nat st $1 = m & len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) holds

Sum x = v;

A1: S

A2: for k being Nat st S

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[k + 1]

for m being non zero Element of NAT

for x being FinSequence of Z_2

for v being Element of Z_2

for j being Nat st k + 1 = m & len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) holds

Sum x = v_{1}[k + 1]
; :: thesis: verum

end;assume A3: S

for m being non zero Element of NAT

for x being FinSequence of Z_2

for v being Element of Z_2

for j being Nat st k + 1 = m & len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) holds

Sum x = v

proof

hence
S
let m be non zero Element of NAT ; :: thesis: for x being FinSequence of Z_2

for v being Element of Z_2

for j being Nat st k + 1 = m & len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) holds

Sum x = v

let x be FinSequence of Z_2; :: thesis: for v being Element of Z_2

for j being Nat st k + 1 = m & len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) holds

Sum x = v

let v be Element of Z_2; :: thesis: for j being Nat st k + 1 = m & len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) holds

Sum x = v

let j be Nat; :: thesis: ( k + 1 = m & len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) implies Sum x = v )

assume A4: ( k + 1 = m & len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) ) ; :: thesis: Sum x = v

reconsider xk = x | k as FinSequence of Z_2 ;

A5: k <= k + 1 by NAT_1:11;

A6: len xk = k by A4, NAT_1:11, FINSEQ_1:59;

A7: len x = (len xk) + 1 by A4, NAT_1:11, FINSEQ_1:59;

A8: xk = x | (dom xk) by A6, FINSEQ_1:def 3;

A9: len ((len xk) |-> (0. Z_2)) = len xk by CARD_1:def 7;

end;for v being Element of Z_2

for j being Nat st k + 1 = m & len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) holds

Sum x = v

let x be FinSequence of Z_2; :: thesis: for v being Element of Z_2

for j being Nat st k + 1 = m & len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) holds

Sum x = v

let v be Element of Z_2; :: thesis: for j being Nat st k + 1 = m & len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) holds

Sum x = v

let j be Nat; :: thesis: ( k + 1 = m & len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) implies Sum x = v )

assume A4: ( k + 1 = m & len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) ) ; :: thesis: Sum x = v

reconsider xk = x | k as FinSequence of Z_2 ;

A5: k <= k + 1 by NAT_1:11;

A6: len xk = k by A4, NAT_1:11, FINSEQ_1:59;

A7: len x = (len xk) + 1 by A4, NAT_1:11, FINSEQ_1:59;

A8: xk = x | (dom xk) by A6, FINSEQ_1:def 3;

A9: len ((len xk) |-> (0. Z_2)) = len xk by CARD_1:def 7;

per cases
( j = m or j <> m )
;

end;

suppose A10:
j = m
; :: thesis: Sum x = v

then A11:
x . (len x) = v
by A4;

for i being Nat st i in dom xk holds

xk . i = ((len xk) |-> (0. Z_2)) . i

thus Sum x = (Sum xk) + v by RLVECT_1:38, A7, A8, A11

.= v + (0. Z_2) by A15, Th4

.= v by BSPACE:5 ; :: thesis: verum

end;for i being Nat st i in dom xk holds

xk . i = ((len xk) |-> (0. Z_2)) . i

proof

then A15:
xk = (len xk) |-> (0. Z_2)
by A9, FINSEQ_2:9;
let i be Nat; :: thesis: ( i in dom xk implies xk . i = ((len xk) |-> (0. Z_2)) . i )

assume A12: i in dom xk ; :: thesis: xk . i = ((len xk) |-> (0. Z_2)) . i

then A13: i in Seg k by A6, FINSEQ_1:def 3;

then A14: i in Seg m by A4, A5, FINSEQ_1:5, TARSKI:def 3;

( 1 <= i & i <= k ) by FINSEQ_1:1, A13;

then i <> j by A4, A10, NAT_1:13;

then x . i = 0. Z_2 by A4, A14;

then xk . i = 0. Z_2 by A12, A8, FUNCT_1:49;

hence xk . i = ((len xk) |-> (0. Z_2)) . i by BSPACE:5; :: thesis: verum

end;assume A12: i in dom xk ; :: thesis: xk . i = ((len xk) |-> (0. Z_2)) . i

then A13: i in Seg k by A6, FINSEQ_1:def 3;

then A14: i in Seg m by A4, A5, FINSEQ_1:5, TARSKI:def 3;

( 1 <= i & i <= k ) by FINSEQ_1:1, A13;

then i <> j by A4, A10, NAT_1:13;

then x . i = 0. Z_2 by A4, A14;

then xk . i = 0. Z_2 by A12, A8, FUNCT_1:49;

hence xk . i = ((len xk) |-> (0. Z_2)) . i by BSPACE:5; :: thesis: verum

thus Sum x = (Sum xk) + v by RLVECT_1:38, A7, A8, A11

.= v + (0. Z_2) by A15, Th4

.= v by BSPACE:5 ; :: thesis: verum

suppose A16:
j <> m
; :: thesis: Sum x = v

A17:
( 1 <= j & j <= m )
by A4, FINSEQ_1:1;

then j < m by A16, XXREAL_0:1;

then j <= k by A4, NAT_1:13;

then A18: j in Seg k by A17;

A19: k <> 0 by A4, A16, XXREAL_0:1, A17;

for i being Nat st i in Seg k holds

( ( i = j implies xk . i = v ) & ( i <> j implies xk . i = 0. Z_2 ) )

A23: m in Seg m by FINSEQ_1:3;

A24: x . (len x) = 0. Z_2 by A4, A23, A16;

thus Sum x = v + (0. Z_2) by RLVECT_1:38, A7, A8, A24, A22

.= v by BSPACE:5 ; :: thesis: verum

end;then j < m by A16, XXREAL_0:1;

then j <= k by A4, NAT_1:13;

then A18: j in Seg k by A17;

A19: k <> 0 by A4, A16, XXREAL_0:1, A17;

for i being Nat st i in Seg k holds

( ( i = j implies xk . i = v ) & ( i <> j implies xk . i = 0. Z_2 ) )

proof

then A22:
Sum xk = v
by A6, A3, A18, A19;
let i be Nat; :: thesis: ( i in Seg k implies ( ( i = j implies xk . i = v ) & ( i <> j implies xk . i = 0. Z_2 ) ) )

assume A20: i in Seg k ; :: thesis: ( ( i = j implies xk . i = v ) & ( i <> j implies xk . i = 0. Z_2 ) )

A21: Seg k c= Seg m by A4, NAT_1:11, FINSEQ_1:5;

xk . i = x . i by A20, FUNCT_1:49;

hence ( ( i = j implies xk . i = v ) & ( i <> j implies xk . i = 0. Z_2 ) ) by A4, A20, A21; :: thesis: verum

end;assume A20: i in Seg k ; :: thesis: ( ( i = j implies xk . i = v ) & ( i <> j implies xk . i = 0. Z_2 ) )

A21: Seg k c= Seg m by A4, NAT_1:11, FINSEQ_1:5;

xk . i = x . i by A20, FUNCT_1:49;

hence ( ( i = j implies xk . i = v ) & ( i <> j implies xk . i = 0. Z_2 ) ) by A4, A20, A21; :: thesis: verum

A23: m in Seg m by FINSEQ_1:3;

A24: x . (len x) = 0. Z_2 by A4, A23, A16;

thus Sum x = v + (0. Z_2) by RLVECT_1:38, A7, A8, A24, A22

.= v by BSPACE:5 ; :: thesis: verum

hence for x being FinSequence of Z_2

for v being Element of Z_2

for j being Nat st len x = m & j in Seg m & ( for i being Nat st i in Seg m holds

( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) holds

Sum x = v ; :: thesis: verum