defpred S_{2}[ 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 ; :: 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 S_{2}[n] holds

S_{2}[n + 1]
_{2}[ 0 ]
;

for n being Nat holds S_{2}[n]
from NAT_1:sch 2(A13, A2);

hence Sum (MIM R) = R . 1 by A1; :: thesis: verum

Sum (MIM R) = R . 1;

let R be FinSequence of REAL ; :: 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 S

S

proof

A13:
S
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume A3: S_{2}[n]
; :: thesis: S_{2}[n + 1]

let R be FinSequence of REAL ; :: 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

end;assume A3: S

let R be FinSequence of REAL ; :: 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 ) )end;

hence
Sum (MIM R) = R . 1
; :: thesis: verumper cases
( n = 0 or n <> 0 )
;

end;

case A5:
n = 0
; :: thesis: Sum (MIM R) = R . 1

A6:
R . 1 in REAL
by XREAL_0:def 1;

A7: R = <*(R . 1)*> by A4, A5, FINSEQ_1:40;

then MIM R = R by Th13;

hence Sum (MIM R) = R . 1 by A7, A6, FINSOP_1:11; :: thesis: verum

end;A7: R = <*(R . 1)*> by A4, A5, FINSEQ_1:40;

then MIM R = R by Th13;

hence Sum (MIM R) = R . 1 by A7, A6, FINSOP_1:11; :: thesis: verum

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:1, 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, FINSEQ_1:1;

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;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:1, 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, FINSEQ_1:1;

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

for n being Nat holds S

hence Sum (MIM R) = R . 1 by A1; :: thesis: verum