defpred S2[ Nat] means for R being FinSequence of REAL st len R <> 0 & len R = $1 holds
Sum (MIM R) = R . 1;
let R be FinSequence of REAL ; ( len R <> 0 implies Sum (MIM R) = R . 1 )
assume A1:
len R <> 0
; Sum (MIM R) = R . 1
A2:
for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be
Nat;
( S2[n] implies S2[n + 1] )
assume A3:
S2[
n]
;
S2[n + 1]
let R be
FinSequence of
REAL ;
( len R <> 0 & len R = n + 1 implies Sum (MIM R) = R . 1 )
assume that
len R <> 0
and A4:
len R = n + 1
;
Sum (MIM R) = R . 1
now ( ( 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
;
Sum (MIM R) = R . 1then
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
;
verum end;
hence
Sum (MIM R) = R . 1
;
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; verum