let rF be real-valued XFinSequence; :: thesis: for r being Real st rF is nonnegative-yielding & len rF > 0 & ex x being object st
( x in dom rF & rF . x = r ) holds
Sum rF >= r
let r be Real; :: thesis: ( rF is nonnegative-yielding & len rF > 0 & ex x being object st
( x in dom rF & rF . x = r ) implies Sum rF >= r )
assume that
A1: rF is nonnegative-yielding and
A2: len rF > 0 and
A3: ex x being object st
( x in dom rF & rF . x = r ) ; :: thesis: Sum rF >= r
consider x being object such that
A4: x in dom rF and
A5: rF . x = r by A3;
reconsider lenrF1 = (len rF) - 1 as Element of NAT by A2, NAT_1:20;
A6: dom rF = lenrF1 + 1 ;
reconsider x = x as Element of NAT by A4;
A7: lenrF1 < lenrF1 + 1 by NAT_1:13;
A8: x < len rF by A4, AFINSQ_1:86;
then A9: x <= lenrF1 by A6, NAT_1:13;
consider f being sequence of REAL such that
A10: f . 0 = rF . 0 and
A11: for n being Nat st n + 1 < len rF holds
f . (n + 1) = addreal . ((f . n),(rF . (n + 1))) and
A12: addreal "**" rF = f . ((len rF) - 1) by Def8, A2;
defpred S₁[ Nat] means ( $1 < x implies f . $1 >= 0 );
0 in len rF by A2, AFINSQ_1:86;
then rF . 0 in rng rF by FUNCT_1:def 3;
then A13: S₁[ 0 ] by A1, A10, PARTFUN3:def 4;
A14: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A15: S₁[n] ; :: thesis: S₁[n + 1]
assume A16: n + 1 < x ; :: thesis: f . (n + 1) >= 0
then ( n < x & n + 1 < len rF ) by A8, NAT_1:13, XXREAL_0:2;
then A17: ( f . (n + 1) = addreal . ((f . n),(rF . (n + 1))) & f . n >= 0 & n + 1 in dom rF ) by A11, A15, AFINSQ_1:86;
then rF . (n + 1) in rng rF by FUNCT_1:def 3;
then rF . (n + 1) >= 0 by A1, PARTFUN3:def 4;
then (f . n) + (rF . (n + 1)) >= zz + zz by A16, A15, NAT_1:13;
hence f . (n + 1) >= 0 by A17, BINOP_2:def 9; :: thesis: verum

end;

A18: for n being Nat holds S₁[n] from NAT_1:sch 2(A13, A14);
defpred S₂[ Nat] means ( x <= $1 & $1 < len rF implies f . $1 >= r );

now :: thesis: ( x <= x & x < len rF implies f . x >= r )

per cases ( x = 0 or x > 0 ) ;

suppose A19: x = 0 ; :: thesis: ( x <= x & x < len rF implies f . x >= r )

assume that
x <= x and
x < len rF ; :: thesis: f . x >= r
thus f . x >= r by A5, A10, A19; :: thesis: verum

end;

suppose x > 0 ; :: thesis: ( x <= x & x < len rF implies f . x >= r )

then reconsider x1 = x - 1 as Element of NAT by NAT_1:20;
assume that
x <= x and
A20: x < len rF ; :: thesis: f . x >= r
A21: x1 < x1 + 1 by NAT_1:13;
x1 + 1 < len rF by A20;
then f . x = addreal . ((f . x1),(rF . x)) by A11;
then ( f . x = (f . x1) + (rF . x) & f . x1 >= 0 ) by A21, A18, BINOP_2:def 9;
then f . x >= r + 0 by A5, XREAL_1:7;
hence f . x >= r ; :: thesis: verum

end;

end;

end;

then A22: S₂[x] ;
A23: for m being Nat st m >= x & S₂[m] holds
S₂[m + 1]

proof

let m be Nat; :: thesis: ( m >= x & S₂[m] implies S₂[m + 1] )
assume that
A24: m >= x and
A25: S₂[m] ; :: thesis: S₂[m + 1]
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
assume that
x <= m + 1 and
A26: m + 1 < len rF ; :: thesis: f . (m + 1) >= r
m + 1 in dom rF by A26, AFINSQ_1:86;
then A27: rF . (m + 1) in rng rF by FUNCT_1:def 3;
f . (m1 + 1) = addreal . ((f . m1),(rF . (m1 + 1))) by A11, A26;
then ( f . (m1 + 1) = (f . m1) + (rF . (m1 + 1)) & rF . (m1 + 1) >= 0 ) by A27, A1, BINOP_2:def 9, PARTFUN3:def 4;
then f . (m + 1) >= r + 0 by A24, A25, A26, NAT_1:13, XREAL_1:7;
hence f . (m + 1) >= r ; :: thesis: verum

end;

for m being Nat st m >= x holds
S₂[m] from NAT_1:sch 8(A22, A23);
then addreal "**" rF >= r by A12, A9, A7;
hence Sum rF >= r by Th47; :: thesis: verum