let k be Element of NAT ; :: thesis: for Fn being XFinSequence of NAT st ( for n being Element of NAT st n in dom Fn holds
Fn . n >= k ) holds
Sum Fn >= (len Fn) * k
let Fn be XFinSequence of NAT ; :: thesis: ( ( for n being Element of NAT st n in dom Fn holds
Fn . n >= k ) implies Sum Fn >= (len Fn) * k )
assume A1: for n being Element of NAT st n in dom Fn holds
Fn . n >= k ; :: thesis: Sum Fn >= (len Fn) * k

now

per cases ( dom Fn = 0 or dom Fn > 0 ) ;

suppose dom Fn = 0 ; :: thesis: Sum Fn >= (len Fn) * k

hence Sum Fn >= (len Fn) * k ; :: thesis: verum

end;

suppose A2: dom Fn > 0 ; :: thesis: Sum Fn >= (len Fn) * k

then consider f being Function of NAT , NAT such that
A3: f . 0 = Fn . 0 and
A4: for n being Element of NAT st n + 1 < len Fn holds
f . (n + 1) = addnat . (f . n),(Fn . (n + 1)) and
A5: addnat "**" Fn = f . ((len Fn) - 1) by Def3;
defpred S₁[ Element of NAT ] means ( $1 < len Fn implies f . $1 >= ($1 + 1) * k );
A6: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A7: S₁[m] ; :: thesis: S₁[m + 1]
assume A8: m + 1 < len Fn ; :: thesis: f . (m + 1) >= ((m + 1) + 1) * k
then f . (m + 1) = addnat . (f . m),(Fn . (m + 1)) by A4;
then A9: f . (m + 1) = (f . m) + (Fn . (m + 1)) by BINOP_2:def 23;
m + 1 in len Fn by A8, NAT_1:45;
then Fn . (m + 1) >= k by A1;
then f . (m + 1) >= ((m + 1) * k) + k by A7, A8, A9, NAT_1:13, XREAL_1:9;
hence f . (m + 1) >= ((m + 1) + 1) * k ; :: thesis: verum

end;

reconsider lenFn1 = (len Fn) - 1 as Element of NAT by A2, NAT_1:20;
A10: lenFn1 < lenFn1 + 1 by NAT_1:13;
A11: S₁[ 0 ]

proof

assume 0 < len Fn ; :: thesis: f . 0 >= (0 + 1) * k
then 0 in dom Fn by NAT_1:45;
hence f . 0 >= (0 + 1) * k by A1, A3; :: thesis: verum

end;

for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A11, A6);
hence Sum Fn >= (len Fn) * k by A5, A10; :: thesis: verum

end;

end;

end;

hence Sum Fn >= (len Fn) * k ; :: thesis: verum