let k be Element of NAT ; :: thesis: for Fn being XFinSequence of NAT 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 NAT ; :: 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 and
A4: Fn . x = k by A2;
reconsider lenFn1 = (len Fn) - 1 as Element of NAT by A1, NAT_1:20;
A5: dom Fn = lenFn1 + 1 ;
reconsider x = x as Element of NAT by A3;
A6: lenFn1 < lenFn1 + 1 by NAT_1:13;
x < dom Fn by A3, NAT_1:45;
then A7: x <= lenFn1 by A5, NAT_1:13;
consider f being Function of NAT , NAT such that
A8: f . 0 = Fn . 0 and
A9: for n being Element of NAT st n + 1 < len Fn holds
f . (n + 1) = addnat . (f . n),(Fn . (n + 1)) and
A10: addnat "**" Fn = f . ((len Fn) - 1) by A1, Def3;
defpred S₁[ Nat] means ( x <= $1 & $1 < len Fn implies f . $1 >= k );

now

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

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

assume that
x <= x and
x < len Fn ; :: thesis: f . x >= k
thus f . x >= k by A4, A8, A11; :: 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 that
x <= x and
A12: x < len Fn ; :: thesis: f . x >= k
x1 + 1 < len Fn by A12;
then f . x = addnat . (f . x1),(Fn . x) by A9;
then f . x = (f . x1) + (Fn . x) by BINOP_2:def 23;
then f . x >= k + 0 by A4, XREAL_1:9;
hence f . x >= k ; :: thesis: verum

end;

end;

end;

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

end;

for m being Nat st m >= x holds
S₁[m] from NAT_1:sch 8(A13, A14);
hence Sum Fn >= k by A10, A7, A6; :: thesis: verum