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 Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be
Element of
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 per cases
( n = 0 or n <> 0 )
;
case
n <> 0
;
Sum (MIM R) = R . 1then
0 < n
by NAT_1:3;
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;
A6:
0 + 1
<= n1 + 1
by NAT_1:11;
then A7:
(
Seg (len R) = dom R & 1
in Seg (n1 + 1) )
by FINSEQ_1:3, FINSEQ_1:def 3;
n1 + 2
= (n1 + 1) + 1
;
then
n1 + 1
<= n1 + 2
by NAT_1:11;
then A8:
n1 + 1
in Seg (n1 + 2)
by A6, FINSEQ_1:3;
set f1 =
R | (n1 + 1);
set s =
R . (n1 + 2);
set r =
R . (n1 + 1);
A9:
n1 + 2
= len R
by A4;
A10:
len (R | (n1 + 1)) = n1 + 1
by A4, FINSEQ_1:80, NAT_1:11;
thus Sum (MIM R) =
Sum (((MIM R) | n1) ^ <*((R . (n1 + 1)) - (R . (n1 + 2))),(R . (n1 + 2))*>)
by A4, Th24
.=
(Sum ((MIM R) | n1)) + (Sum <*((R . (n1 + 1)) - (R . (n1 + 2))),(R . (n1 + 2))*>)
by RVSUM_1:105
.=
(Sum ((MIM R) | n1)) + (((R . (n1 + 1)) - (R . (n1 + 2))) + (R . (n1 + 2)))
by RVSUM_1:107
.=
Sum (((MIM R) | n1) ^ <*(R . (n1 + 1))*>)
by RVSUM_1:104
.=
Sum (MIM (R | (n1 + 1)))
by A9, Th23
.=
(R | (n1 + 1)) . 1
by A3, A10
.=
R . 1
by A4, A8, A7, Th19
;
verum end;
hence
Sum (MIM R) = R . 1
;
verum
end;
A11:
S2[ 0 ]
;
for n being Element of NAT holds S2[n]
from NAT_1:sch 1(A11, A2);
hence
Sum (MIM R) = R . 1
by A1; verum