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 S1[ 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: S1[ 0 ] ;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[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 ;
A7: len x = (len xk) + 1 by ;
A8: xk = x | (dom xk) by ;
A9: len ((len xk) |-> ()) = 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) |-> ()) . i
proof
let i be Nat; :: thesis: ( i in dom xk implies xk . i = ((len xk) |-> ()) . i )
assume A12: i in dom xk ; :: thesis: xk . i = ((len xk) |-> ()) . i
then A13: i in Seg k by ;
then A14: i in Seg m by ;
( 1 <= i & i <= k ) by ;
then i <> j by ;
then x . i = 0. Z_2 by ;
then xk . i = 0. Z_2 by ;
hence xk . i = ((len xk) |-> ()) . i by BSPACE:5; :: thesis: verum
end;
then A15: xk = (len xk) |-> () by ;
thus Sum x = (Sum xk) + v by
.= v + () by
.= v by BSPACE:5 ; :: thesis: verum
end;
suppose A16: j <> m ; :: thesis: Sum x = v
A17: ( 1 <= j & j <= m ) by ;
then j < m by ;
then j <= k by ;
then A18: j in Seg k by A17;
A19: k <> 0 by ;
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 ;
xk . i = x . i by ;
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 + () by
.= v by BSPACE:5 ; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
for k being Nat holds S1[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