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
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 );
A3: S1[ 0 ]
proof
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
A4: 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 N = 0. ; :: thesis: ( N = 0 & Sum F = N * p )
consider f being Function of NAT ,ExtREAL such that
A5: ( Sum F = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) by CONVFUN1:def 5;
thus ( N = 0 & Sum F = N * p ) by A4, A5; :: thesis: verum
end;
hence S1[ 0 ] ; :: thesis: verum
end;
A6: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A7: S1[k] ; :: thesis: S1[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def 13;
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
A8: k + 1 = len F and
A9: 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 A8;
then consider G being FinSequence, v being set such that
A10: F = G ^ <*v*> by FINSEQ_1:63;
reconsider G = G as FinSequence of ExtREAL by A10, FINSEQ_1:50;
A11: k + 1 = (len G) + (len <*v*>) by A8, A10, FINSEQ_1:35
.= (len G) + 1 by FINSEQ_1:56 ;
dom <*v*> = Seg 1 by FINSEQ_1:55;
then A12: 1 in dom <*v*> by FINSEQ_1:4, TARSKI:def 1;
1 <= k + 1 by NAT_1:11;
then A13: k + 1 in dom F by A8, FINSEQ_3:27;
v = <*v*> . 1 by FINSEQ_1:57
.= F . (k + 1) by A10, A11, A12, FINSEQ_1:def 7
.= p by A9, A13 ;
then reconsider v = v as Element of ExtREAL ;
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 )
assume A14: n in dom G ; :: thesis: G . n = p
then A15: ( 1 <= n & n <= len G ) by FINSEQ_3:27;
len G <= (len G) + 1 by NAT_1:11;
then A16: ( 1 <= n & n <= (len G) + 1 ) by A15, XXREAL_0:2;
len F = (len G) + (len <*v*>) by A10, FINSEQ_1:35
.= (len G) + 1 by FINSEQ_1:56 ;
then n in dom F by A16, FINSEQ_3:27;
then F . n = p by A9;
hence G . n = p by A10, A14, FINSEQ_1:def 7; :: thesis: verum
end;
then consider N1 being Element of ExtREAL such that
A17: ( N1 = k & Sum G = N1 * p ) by A7, A11;
consider f being Function of NAT ,ExtREAL such that
A18: ( Sum F = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) by CONVFUN1:def 5;
consider g being Function of NAT ,ExtREAL such that
A19: ( Sum G = g . (len G) & g . 0 = 0. & ( for i being Element of NAT st i < len G holds
g . (i + 1) = (g . i) + (G . (i + 1)) ) ) by CONVFUN1:def 5;
A20: 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 );
A21: S2[ 0 ] by A18, A19;
A22: for k1 being Nat st S2[k1] holds
S2[k1 + 1]
proof
let k1 be Nat; :: thesis: ( S2[k1] implies S2[k1 + 1] )
assume A23: S2[k1] ; :: thesis: S2[k1 + 1]
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
now
assume A24: k1 + 1 <= len G ; :: thesis: S2[k1 + 1]
A25: k1 <= k1 + 1 by NAT_1:11;
A26: k1 < len G by A24, NAT_1:13;
then A27: g . (k1 + 1) = (g . k1) + (G . (k1 + 1)) by A19;
len F = (len G) + (len <*v*>) by A10, FINSEQ_1:35
.= (len G) + 1 by FINSEQ_1:56 ;
then k1 < len F by A26, NAT_1:13;
then A28: f . (k1 + 1) = (f . k1) + (F . (k1 + 1)) by A18;
1 <= k1 + 1 by NAT_1:11;
then k1 + 1 in dom G by A24, FINSEQ_3:27;
hence S2[k1 + 1] by A10, A23, A25, A27, A28, FINSEQ_1:def 7, XXREAL_0:2; :: thesis: verum
end;
hence S2[k1 + 1] ; :: thesis: verum
end;
for k1 being Nat holds S2[k1] from NAT_1:sch 2(A21, A22);
 hence for k1 being Nat st k1 <= len G holds
f . k1 = g . k1 ; :: thesis: verum
end;
k < len F by A8, NAT_1:13;
then Sum F = (f . k) + (F . (k + 1)) by A8, A18
.= (g . k) + (F . (k + 1)) by A11, A20 ;
then A29: Sum F = (Sum G) + p by A9, A11, A13, A19
.= (N1 * p) + (1. * p) by A17, XXREAL_3:92 ;
take N = N1 + 1. ; :: thesis: ( N = k + 1 & Sum F = N * p )
( N = k + 1 & Sum F = N * p ) by A17, A29, SUPINF_2:1, XXREAL_3:107;
hence ( N = k + 1 & Sum F = N * p ) ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A3, A6);
 then consider N' being Element of ExtREAL such that
A30: ( N' = len a & Sum a = N' * p ) by A2;
thus Sum a = N * p by A1, A30; :: thesis: verum