defpred S2[ Nat] means for R being real-valued FinSequence st len R <> 0 & len R = $1 holds
Sum (MIM R) = R . 1;
let R be real-valued FinSequence; :: thesis: ( len R <> 0 implies Sum (MIM R) = R . 1 )
assume A1: len R <> 0 ; :: thesis: Sum (MIM R) = R . 1
A2: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A3: S2[n] ; :: thesis: S2[n + 1]
let R be real-valued FinSequence; :: thesis: ( len R <> 0 & len R = n + 1 implies Sum (MIM R) = R . 1 )
assume that
len R <> 0 and
A4: len R = n + 1 ; :: thesis: Sum (MIM R) = R . 1
now :: thesis: ( ( n = 0 & Sum (MIM R) = R . 1 ) or ( n <> 0 & Sum (MIM R) = R . 1 ) )
per cases ( n = 0 or n <> 0 ) ;
case n <> 0 ; :: thesis: Sum (MIM R) = R . 1
then 0 < n ;
then 0 + 1 <= n by NAT_1:13;
then max (0,(n - 1)) = n - 1 by FINSEQ_2:4;
then reconsider n1 = n - 1 as Element of NAT by FINSEQ_2:5;
A8: 0 + 1 <= n1 + 1 by NAT_1:11;
then A9: ( Seg (len R) = dom R & 1 in Seg (n1 + 1) ) by FINSEQ_1:def 3;
n1 + 2 = (n1 + 1) + 1 ;
then n1 + 1 <= n1 + 2 by NAT_1:11;
then A10: n1 + 1 in Seg (n1 + 2) by A8;
set f1 = R | (n1 + 1);
set s = R . (n1 + 2);
set r = R . (n1 + 1);
A11: n1 + 2 = len R by A4;
A12: len (R | (n1 + 1)) = n1 + 1 by A4, FINSEQ_1:59, NAT_1:11;
thus Sum (MIM R) = Sum (((MIM R) | n1) ^ <*((R . (n1 + 1)) - (R . (n1 + 2))),(R . (n1 + 2))*>) by A4, Th11
.= (Sum ((MIM R) | n1)) + (Sum <*((R . (n1 + 1)) - (R . (n1 + 2))),(R . (n1 + 2))*>) by RVSUM_1:75
.= (Sum ((MIM R) | n1)) + (((R . (n1 + 1)) - (R . (n1 + 2))) + (R . (n1 + 2))) by RVSUM_1:77
.= Sum (((MIM R) | n1) ^ <*(R . (n1 + 1))*>) by RVSUM_1:74
.= Sum (MIM (R | (n1 + 1))) by A11, Th10
.= (R | (n1 + 1)) . 1 by A3, A12
.= R . 1 by A4, A10, A9, Th6 ; :: thesis: verum
end;
end;
end;
hence Sum (MIM R) = R . 1 ; :: thesis: verum
end;
A13: S2[ 0 ] ;
for n being Nat holds S2[n] from NAT_1:sch 2(A13, A2);
 hence Sum (MIM R) = R . 1 by A1; :: thesis: verum