defpred S1[ Nat] means for F being FinSequence of ExtREAL
for p being Element of ExtREAL st $1 = len F & ( for n being Nat st n in dom F holds
F . n = p ) holds
ex N being Element of ExtREAL st
( N = $1 & Sum F = N * p );
let a be FinSequence of ExtREAL ; :: thesis: for p, N being Element of ExtREAL st N = len a & ( for n being Nat st n in dom a holds
a . n = p ) holds
Sum a = N * p
let p, N be Element of ExtREAL ; :: thesis: ( N = len a & ( for n being Nat st n in dom a holds
a . n = p ) implies Sum a = N * p )
assume that
A1: N = len a and
A2: for n being Nat st n in dom a holds
a . n = p ; :: thesis: Sum a = N * p
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def 12;
for F being FinSequence of ExtREAL
for p being Element of ExtREAL st k + 1 = len F & ( for n being Nat st n in dom F holds
F . n = p ) holds
ex N being Element of ExtREAL st
( N = k + 1 & Sum F = N * p )
proof
let F be FinSequence of ExtREAL ; :: thesis: for p being Element of ExtREAL st k + 1 = len F & ( for n being Nat st n in dom F holds
F . n = p ) holds
ex N being Element of ExtREAL st
( N = k + 1 & Sum F = N * p )
let p be Element of ExtREAL ; :: thesis: ( k + 1 = len F & ( for n being Nat st n in dom F holds
F . n = p ) implies ex N being Element of ExtREAL st
( N = k + 1 & Sum F = N * p ) )
assume that
A5: k + 1 = len F and
A6: for n being Nat st n in dom F holds
F . n = p ; :: thesis: ex N being Element of ExtREAL st
( N = k + 1 & Sum F = N * p )
F <> {} by A5;
then consider G being FinSequence, v being object such that
A7: F = G ^ <*v*> by FINSEQ_1:46;
reconsider G = G as FinSequence of ExtREAL by A7, FINSEQ_1:36;
A8: k + 1 = (len G) + (len <*v*>) by A5, A7, FINSEQ_1:22
.= (len G) + 1 by FINSEQ_1:39 ;
dom <*v*> = Seg 1 by FINSEQ_1:38;
then A9: 1 in dom <*v*> by FINSEQ_1:2, TARSKI:def 1;
1 <= k + 1 by NAT_1:11;
then A10: k + 1 in dom F by A5, FINSEQ_3:25;
v = <*v*> . 1
.= F . (k + 1) by A7, A8, A9, FINSEQ_1:def 7
.= p by A6, A10 ;
then reconsider v = v as Element of ExtREAL ;
consider g being sequence of ExtREAL such that
A11: Sum G = g . (len G) and
A12: g . 0 = 0. and
A13: for i being Nat st i < len G holds
g . (i + 1) = (g . i) + (G . (i + 1)) by EXTREAL1:def 2;
for n being Nat st n in dom G holds
G . n = p
proof
let n be Nat; :: thesis: ( n in dom G implies G . n = p )
A14: len G <= (len G) + 1 by NAT_1:11;
assume A15: n in dom G ; :: thesis: G . n = p
then n <= len G by FINSEQ_3:25;
then A16: n <= (len G) + 1 by A14, XXREAL_0:2;
A17: len F = (len G) + (len <*v*>) by A7, FINSEQ_1:22
.= (len G) + 1 by FINSEQ_1:39 ;
1 <= n by A15, FINSEQ_3:25;
then n in dom F by A16, A17, FINSEQ_3:25;
then F . n = p by A6;
hence G . n = p by A7, A15, FINSEQ_1:def 7; :: thesis: verum
end;
then consider N1 being Element of ExtREAL such that
A18: N1 = k and
A19: Sum G = N1 * p by A4, A8;
consider f being sequence of ExtREAL such that
A20: Sum F = f . (len F) and
A21: f . 0 = 0. and
A22: for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) by EXTREAL1:def 2;
A23: for k1 being Nat st k1 <= len G holds
f . k1 = g . k1
proof
defpred S2[ Nat] means ( $1 <= len G implies f . $1 = g . $1 );
A24: for k1 being Nat st S2[k1] holds
S2[k1 + 1]
proof
let k1 be Nat; :: thesis: ( S2[k1] implies S2[k1 + 1] )
assume A25: S2[k1] ; :: thesis: S2[k1 + 1]
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;
now :: thesis: ( k1 + 1 <= len G implies S2[k1 + 1] )
assume A26: k1 + 1 <= len G ; :: thesis: S2[k1 + 1]
then A27: k1 < len G by NAT_1:13;
len F = (len G) + (len <*v*>) by A7, FINSEQ_1:22
.= (len G) + 1 by FINSEQ_1:39 ;
then k1 < len F by A27, NAT_1:13;
then A28: f . (k1 + 1) = (f . k1) + (F . (k1 + 1)) by A22;
1 <= k1 + 1 by NAT_1:11;
then A29: k1 + 1 in dom G by A26, FINSEQ_3:25;
( k1 <= k1 + 1 & g . (k1 + 1) = (g . k1) + (G . (k1 + 1)) ) by A13, A27, NAT_1:11;
hence S2[k1 + 1] by A7, A25, A28, A29, FINSEQ_1:def 7, XXREAL_0:2; :: thesis: verum
end;
hence S2[k1 + 1] ; :: thesis: verum
end;
A30: S2[ 0 ] by A21, A12;
for k1 being Nat holds S2[k1] from NAT_1:sch 2(A30, A24);
 hence for k1 being Nat st k1 <= len G holds
f . k1 = g . k1 ; :: thesis: verum
end;
take N1 + 1. ; :: thesis: ( N1 + 1. = k + 1 & Sum F = (N1 + 1.) * p )
reconsider jj = 1 as Real ;
thus N1 + 1. = k + jj by A18, SUPINF_2:1
.= k + 1 ; :: thesis: Sum F = (N1 + 1.) * p
k < len F by A5, NAT_1:13;
then Sum F = (f . k) + (F . (k + 1)) by A5, A20, A22
.= (g . k) + (F . (k + 1)) by A8, A23 ;
then Sum F = (Sum G) + p by A6, A8, A10, A11
.= (N1 * p) + (1. * p) by A19, XXREAL_3:81 ;
hence Sum F = (N1 + 1.) * p by A18, XXREAL_3:96; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
for F being FinSequence of ExtREAL
for p being Element of ExtREAL st 0 = len F & ( for n being Nat st n in dom F holds
F . n = p ) holds
ex N being Element of ExtREAL st
( N = 0 & Sum F = N * p )
proof
let F be FinSequence of ExtREAL ; :: thesis: for p being Element of ExtREAL st 0 = len F & ( for n being Nat st n in dom F holds
F . n = p ) holds
ex N being Element of ExtREAL st
( N = 0 & Sum F = N * p )
let p be Element of ExtREAL ; :: thesis: ( 0 = len F & ( for n being Nat st n in dom F holds
F . n = p ) implies ex N being Element of ExtREAL st
( N = 0 & Sum F = N * p ) )
assume that
A31: 0 = len F and
for n being Nat st n in dom F holds
F . n = p ; :: thesis: ex N being Element of ExtREAL st
( N = 0 & Sum F = N * p )
take 0. ; :: thesis: ( 0. = 0 & Sum F = 0. * p )
ex f being sequence of ExtREAL st
( Sum F = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) by EXTREAL1:def 2;
hence ( 0. = 0 & Sum F = 0. * p ) by A31; :: thesis: verum
end;
then A32: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A32, A3);
 then ex N9 being Element of ExtREAL st
( N9 = len a & Sum a = N9 * p ) by A2;
hence Sum a = N * p by A1; :: thesis: verum