let k be Element of NAT ; :: thesis: for Fn being XFinSequence of 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 ; :: 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 B2: 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: 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;

A7: 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 A8: S₁[m] ; :: thesis: S₁[m + 1]
assume m + 1 < len Fn ; :: thesis: f . (m + 1) >= ((m + 1) + 1) * k
then ( m < len Fn & m + 1 in len Fn & len Fn = dom Fn & f . (m + 1) = addnat . (f . m),(Fn . (m + 1)) ) by A4, NAT_1:13, NAT_1:45;
then ( f . m >= (m + 1) * k & Fn . (m + 1) >= k & f . (m + 1) = (f . m) + (Fn . (m + 1)) ) by A1, A8, BINOP_2:def 23;
then f . (m + 1) >= ((m + 1) * k) + k by XREAL_1:9;
hence f . (m + 1) >= ((m + 1) + 1) * k ; :: thesis: verum

end;

A9: for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A6, A7);
reconsider lenFn1 = (len Fn) - 1 as Element of NAT by B2, NAT_1:20;
lenFn1 < lenFn1 + 1 by NAT_1:13;
hence Sum Fn >= (len Fn) * k by A5, A9; :: thesis: verum

end;

end;

end;

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