let m be non zero Nat; :: thesis: for s, t being FinSequence of REAL m st 1 <= len s & s = t | (len s) holds
for i being Nat st 1 <= i & i <= len s holds
(accum t) . i = (accum s) . i
let s, t be FinSequence of REAL m; :: thesis: ( 1 <= len s & s = t | (len s) implies for i being Nat st 1 <= i & i <= len s holds
(accum t) . i = (accum s) . i )
assume A1: ( 1 <= len s & s = t | (len s) ) ; :: thesis: for i being Nat st 1 <= i & i <= len s holds
(accum t) . i = (accum s) . i
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len s implies (accum t) . $1 = (accum s) . $1 );
A2: S₁[ 0 ] ;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
assume A5: ( 1 <= n + 1 & n + 1 <= len s ) ; :: thesis: (accum t) . (n + 1) = (accum s) . (n + 1)
then A6: n < len s by XXREAL_0:2, NAT_1:16;
A8: 1 in Seg (len s) by A1;

per cases ( n = 0 or n <> 0 ) ;

suppose A7: n = 0 ; :: thesis: (accum t) . (n + 1) = (accum s) . (n + 1)

hence (accum t) . (n + 1) = t . 1 by EUCLID_7:def 10
.= s . 1 by A1, A8, FUNCT_1:49
.= (accum s) . (n + 1) by A7, EUCLID_7:def 10 ;
:: thesis: verum

end;

suppose A9: n <> 0 ; :: thesis: (accum t) . (n + 1) = (accum s) . (n + 1)

then A10: 1 <= n by NAT_1:14;
A11: len (accum t) = len t by EUCLID_7:def 10;
A12: len (accum s) = len s by EUCLID_7:def 10;
n in Seg (len s) by A6, A10;
then A16: n in dom (accum s) by A12, FINSEQ_1:def 3;
A13: len s <= len t by A1, FINSEQ_1:79;
then A14: n < len t by A6, XXREAL_0:2;
then n in Seg (len t) by A10;
then n in dom (accum t) by A11, FINSEQ_1:def 3;
then A17: (accum t) /. n = (accum t) . n by PARTFUN1:def 6
.= (accum s) /. n by A4, A5, A9, A16, PARTFUN1:def 6, XXREAL_0:2, NAT_1:14, NAT_1:16 ;
A18: n + 1 in Seg (len s) by A5;
then A19: n + 1 in dom s by FINSEQ_1:def 3;
n + 1 in Seg (len t) by A18, A13, FINSEQ_1:5, TARSKI:def 3;
then n + 1 in dom t by FINSEQ_1:def 3;
then A21: t /. (n + 1) = t . (n + 1) by PARTFUN1:def 6
.= s . (n + 1) by A1, A18, FUNCT_1:49
.= s /. (n + 1) by A19, PARTFUN1:def 6 ;
thus (accum t) . (n + 1) = ((accum s) /. n) + (t /. (n + 1)) by A9, A14, A17, NAT_1:14, EUCLID_7:def 10
.= (accum s) . (n + 1) by A6, A9, A21, NAT_1:14, EUCLID_7:def 10 ; :: thesis: verum

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence for i being Nat st 1 <= i & i <= len s holds
(accum t) . i = (accum s) . i ; :: thesis: verum