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₁[ 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₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[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

proof

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;

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

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

proof

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;

then A15: xk = (len xk) |-> (0. Z_2) by A9, FINSEQ_2:9;
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;

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

proof

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;

then A22: Sum xk = v by A6, A3, A18, A19;
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;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[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