let rF be real-valued XFinSequence; :: thesis: for r being real number st rF is nonnegative-yielding & len rF > 0 & ex x being set st
( x in dom rF & rF . x = r ) holds
Sum rF >= r
let r be real number ; :: thesis: ( rF is nonnegative-yielding & len rF > 0 & ex x being set 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 set st
( x in dom rF & rF . x = r ) ; :: thesis: Sum rF >= r
consider x being set such that
A5: x in dom rF and
A6: rF . x = r by A3;
reconsider lenrF1 = (len rF) - 1 as Element of NAT by A2, NAT_1:20;
A7: dom rF = lenrF1 + 1 ;
reconsider x = x as Element of NAT by A5;
A8: lenrF1 < lenrF1 + 1 by NAT_1:13;
A9: x < dom rF by A5, NAT_1:45;
then A10: x <= lenrF1 by A7, NAT_1:13;
rF is REAL -valued by Lm7;
then consider f being Function of NAT ,REAL such that
A11: f . 0 = rF . 0 and
A12: for n being Nat st n + 1 < len rF holds
f . (n + 1) = addreal . (f . n),(rF . (n + 1)) and
A13: addreal "**" rF = f . ((len rF) - 1) by Def9, A2;
defpred S₁[ Nat] means ( $1 < x implies f . $1 >= 0 );
0 in len rF by A2, NAT_1:45;
then rF . 0 in rng rF by FUNCT_1:def 5;
then A14: S₁[ 0 ] by A1, PARTFUN3:def 4, A11;
A15: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A16: S₁[n] ; :: thesis: S₁[n + 1]
assume K1: n + 1 < x ; :: thesis: f . (n + 1) >= 0
then ( n < x & n + 1 < len rF ) by NAT_1:13, A9, XXREAL_0:2;
then A18: ( f . (n + 1) = addreal . (f . n),(rF . (n + 1)) & f . n >= 0 & n + 1 in dom rF ) by A12, A16, NAT_1:45;
then rF . (n + 1) in rng rF by FUNCT_1:def 5;
then rF . (n + 1) >= 0 by PARTFUN3:def 4, A1;
then (f . n) + (rF . (n + 1)) >= 0 + 0 by K1, NAT_1:13, A16;
hence f . (n + 1) >= 0 by A18, BINOP_2:def 9; :: thesis: verum

end;

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

now

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

suppose A20: 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 A6, A11, A20; :: 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
A21: x < len rF ; :: thesis: f . x >= r
A22: x1 < x1 + 1 by NAT_1:13;
x1 + 1 < len rF by A21;
then f . x = addreal . (f . x1),(rF . x) by A12;
then ( f . x = (f . x1) + (rF . x) & f . x1 >= 0 ) by BINOP_2:def 9, A22, A19;
then f . x >= r + 0 by A6, XREAL_1:9;
hence f . x >= r ; :: thesis: verum

end;

end;

end;

then A25: S₂[x] ;
A26: 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
A27: m >= x and
A28: S₂[m] ; :: thesis: S₂[m + 1]
reconsider m1 = m as Element of NAT by ORDINAL1:def 13;
assume that
x <= m + 1 and
A29: m + 1 < len rF ; :: thesis: f . (m + 1) >= r
m + 1 in dom rF by NAT_1:45, A29;
then A31: rF . (m + 1) in rng rF by FUNCT_1:def 5;
f . (m1 + 1) = addreal . (f . m1),(rF . (m1 + 1)) by A12, A29;
then ( f . (m1 + 1) = (f . m1) + (rF . (m1 + 1)) & rF . (m1 + 1) >= 0 ) by BINOP_2:def 9, A31, PARTFUN3:def 4, A1;
then f . (m + 1) >= r + 0 by A27, A28, A29, NAT_1:13, XREAL_1:9;
hence f . (m + 1) >= r ; :: thesis: verum

end;

for m being Nat st m >= x holds
S₂[m] from NAT_1:sch 8(A25, A26);
then addreal "**" rF >= r by A13, A10, A8;
hence Sum rF >= r by Th61; :: thesis: verum