let R be FinSequence of REAL ; :: thesis: ( len R <> 0 implies Sum (MIM R) = R . 1 )
defpred S2[ Nat] means for R being FinSequence of REAL st len R <> 0 & len R = $1 holds
Sum (MIM R) = R . 1;
A1:
S2[ 0 ]
;
A2:
for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be
Element of
NAT ;
:: thesis: ( S2[n] implies S2[n + 1] )
assume A3:
S2[
n]
;
:: thesis: S2[n + 1]
let R be
FinSequence of
REAL ;
:: thesis: ( len R <> 0 & len R = n + 1 implies Sum (MIM R) = R . 1 )
assume A4:
(
len R <> 0 &
len R = n + 1 )
;
:: thesis: Sum (MIM R) = R . 1
now per cases
( n = 0 or n <> 0 )
;
case
n <> 0
;
:: thesis: 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:
n1 + 2
= (n1 + 1) + 1
;
A7:
n1 + 2
= len R
by A4;
A8:
(
0 + 1
<= n1 + 1 &
n1 + 1
<= n1 + 2 )
by A6, NAT_1:11;
then A9:
n1 + 1
in Seg (n1 + 2)
by FINSEQ_1:3;
set r =
R . (n1 + 1);
set s =
R . (n1 + 2);
set f1 =
R | (n1 + 1);
A10:
len (R | (n1 + 1)) = n1 + 1
by A4, FINSEQ_1:80, NAT_1:11;
A11:
(
Seg (len R) = dom R & 1
in Seg (n1 + 1) )
by A8, FINSEQ_1:3, FINSEQ_1:def 3;
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 A7, Th23
.=
(R | (n1 + 1)) . 1
by A3, A10
.=
R . 1
by A4, A9, A11, Th19
;
:: thesis: verum end;
hence
Sum (MIM R) = R . 1
;
:: thesis: verum
end;
A12:
for n being Element of NAT holds S2[n]
from NAT_1:sch 1(A1, A2);
assume
len R <> 0
; :: thesis: Sum (MIM R) = R . 1
hence
Sum (MIM R) = R . 1
by A12; :: thesis: verum