let n, j be Nat; :: thesis: for R1, R2 being Real_Sequence st ( for i being Nat st i <= n & not i = j holds
R1 . i = R2 . i ) & j <= n holds
(Sum (R1,n)) - (R1 . j) = (Sum (R2,n)) - (R2 . j)
let R1, R2 be Real_Sequence; :: thesis: ( ( for i being Nat st i <= n & not i = j holds
R1 . i = R2 . i ) & j <= n implies (Sum (R1,n)) - (R1 . j) = (Sum (R2,n)) - (R2 . j) )
A1: CastNat n = n by MODELC_2:def 1;
defpred S₁[ Nat] means ( ( for i being Nat st i <= $1 & not i = j holds
R1 . i = R2 . i ) & j <= $1 implies (Sum (R1,(CastNat $1))) - (R1 . j) = (Sum (R2,(CastNat $1))) - (R2 . j) );
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]
S₁[k + 1]

proof

A4: CastNat k = k by MODELC_2:def 1;
set m = k + 1;
assume that
A5: for i being Nat st i <= k + 1 & not i = j holds
R1 . i = R2 . i and
A6: j <= k + 1 ; :: thesis: (Sum (R1,(CastNat (k + 1)))) - (R1 . j) = (Sum (R2,(CastNat (k + 1)))) - (R2 . j)
reconsider k = k as Element of NAT by ORDINAL1:def 12;

now :: thesis: (Sum (R1,(CastNat (k + 1)))) - (R1 . j) = (Sum (R2,(CastNat (k + 1)))) - (R2 . j)

per cases ( j <= k or j = k + 1 ) by A6, NAT_1:8;

suppose A7: j <= k ; :: thesis: (Sum (R1,(CastNat (k + 1)))) - (R1 . j) = (Sum (R2,(CastNat (k + 1)))) - (R2 . j)

then A8: j < k + 1 by NAT_1:13;
(Sum (R1,(CastNat (k + 1)))) - (R1 . j) = (Sum (R1,(k + 1))) - (R1 . j) by MODELC_2:def 1
.= ((Sum (R1,k)) + (R1 . (k + 1))) - (R1 . j) by SERIES_1:def 1
.= ((Sum (R1,k)) - (R1 . j)) + (R1 . (k + 1))
.= ((Sum (R2,k)) - (R2 . j)) + (R2 . (k + 1)) by A3, A5, A4, A7, A8, NAT_1:12
.= ((Sum (R2,k)) + (R2 . (k + 1))) - (R2 . j)
.= (Sum (R2,(k + 1))) - (R2 . j) by SERIES_1:def 1 ;
hence (Sum (R1,(CastNat (k + 1)))) - (R1 . j) = (Sum (R2,(CastNat (k + 1)))) - (R2 . j) by MODELC_2:def 1; :: thesis: verum

end;

suppose A9: j = k + 1 ; :: thesis: (Sum (R1,(CastNat (k + 1)))) - (R1 . j) = (Sum (R2,(CastNat (k + 1)))) - (R2 . j)

A10: for i being Nat st i <= k holds
R1 . i = R2 . i

proof

let i be Nat; :: thesis: ( i <= k implies R1 . i = R2 . i )
assume A11: i <= k ; :: thesis: R1 . i = R2 . i
i < j by A9, A11, NAT_1:13;
hence R1 . i = R2 . i by A5, A11, NAT_1:12; :: thesis: verum

end;

(Sum (R1,(CastNat (k + 1)))) - (R1 . j) = (Sum (R1,(k + 1))) - (R1 . j) by MODELC_2:def 1
.= ((Sum (R1,k)) + (R1 . (k + 1))) - (R1 . j) by SERIES_1:def 1
.= ((Sum (R2,k)) + (R2 . (k + 1))) - (R2 . j) by A9, A10, Lm25
.= (Sum (R2,(k + 1))) - (R2 . j) by SERIES_1:def 1 ;
hence (Sum (R1,(CastNat (k + 1)))) - (R1 . j) = (Sum (R2,(CastNat (k + 1)))) - (R2 . j) by MODELC_2:def 1; :: thesis: verum

end;

end;

end;

hence (Sum (R1,(CastNat (k + 1)))) - (R1 . j) = (Sum (R2,(CastNat (k + 1)))) - (R2 . j) ; :: thesis: verum

end;

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

end;

A12: S₁[ 0 ]

proof

A13: Sum (R2,(CastNat 0)) = Sum (R2,0) by MODELC_2:def 1
.= R2 . 0 by SERIES_1:def 1 ;
assume that
for i being Nat st i <= 0 & not i = j holds
R1 . i = R2 . i and
A14: j <= 0 ; :: thesis: (Sum (R1,(CastNat 0))) - (R1 . j) = (Sum (R2,(CastNat 0))) - (R2 . j)
A15: Sum (R1,(CastNat 0)) = Sum (R1,0) by MODELC_2:def 1
.= R1 . 0 by SERIES_1:def 1 ;
j = 0 by A14;
hence (Sum (R1,(CastNat 0))) - (R1 . j) = (Sum (R2,(CastNat 0))) - (R2 . j) by A15, A13; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A12, A2);
hence ( ( for i being Nat st i <= n & not i = j holds
R1 . i = R2 . i ) & j <= n implies (Sum (R1,n)) - (R1 . j) = (Sum (R2,n)) - (R2 . j) ) by A1; :: thesis: verum