let k be Element of NAT ; :: thesis: for Fn being XFinSequence of st len Fn > 0 & ex x being set st
( x in dom Fn & Fn . x = k ) holds
Sum Fn >= k
let Fn be XFinSequence of ; :: thesis: ( len Fn > 0 & ex x being set st
( x in dom Fn & Fn . x = k ) implies Sum Fn >= k )
assume that
A1: len Fn > 0 and
A2: ex x being set st
( x in dom Fn & Fn . x = k ) ; :: thesis: Sum Fn >= k
consider x being set such that
A3: ( x in dom Fn & Fn . x = k ) by A2;
reconsider x = x as Element of NAT by A3;
reconsider lenFn1 = (len Fn) - 1 as Element of NAT by A1, NAT_1:20;
consider f being Function of NAT ,NAT such that
A4: f . 0 = Fn . 0 and
A5: for n being Element of NAT st n + 1 < len Fn holds
f . (n + 1) = addnat . (f . n),(Fn . (n + 1)) and
A6: addnat "**" Fn = f . ((len Fn) - 1) by A1, Def3;
defpred S₁[ Nat] means ( x <= $1 & $1 < len Fn implies f . $1 >= k );
A7: S₁[x]

proof

now

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

suppose A8: x = 0 ; :: thesis: ( x <= x & x < len Fn implies f . x >= k )

assume ( x <= x & x < len Fn ) ; :: thesis: f . x >= k
thus f . x >= k by A3, A4, A8; :: thesis: verum

end;

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

then reconsider x1 = x - 1 as Element of NAT by NAT_1:20;
assume ( x <= x & x < len Fn ) ; :: thesis: f . x >= k
then x1 + 1 < len Fn ;
then f . x = addnat . (f . x1),(Fn . x) by A5;
then ( f . x = (f . x1) + (Fn . x) & f . x1 >= 0 ) by BINOP_2:def 23;
then f . x >= k + 0 by A3, XREAL_1:9;
hence f . x >= k ; :: thesis: verum

end;

end;

end;

hence S₁[x] ; :: thesis: verum

end;

A9: 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 A10: ( m >= x & S₁[m] ) ; :: thesis: S₁[m + 1]
reconsider m1 = m as Element of NAT by ORDINAL1:def 13;
assume ( x <= m + 1 & m + 1 < len Fn ) ; :: thesis: f . (m + 1) >= k
then ( f . (m1 + 1) = addnat . (f . m1),(Fn . (m1 + 1)) & m1 < len Fn ) by A5, NAT_1:13;
then ( f . (m1 + 1) = (f . m1) + (Fn . (m1 + 1)) & f . m1 >= k & Fn . (m1 + 1) >= 0 ) by A10, BINOP_2:def 23;
then f . (m + 1) >= k + 0 by XREAL_1:9;
hence f . (m + 1) >= k ; :: thesis: verum

end;

A11: for m being Nat st m >= x holds
S₁[m] from NAT_1:sch 8(A7, A9);
( x < dom Fn & dom Fn = lenFn1 + 1 ) by A3, NAT_1:45;
then ( x <= lenFn1 & lenFn1 < lenFn1 + 1 ) by NAT_1:13;
hence Sum Fn >= k by A6, A11; :: thesis: verum