thus ( f is with_values_greater_or_equal_one implies for n being Nat st 1 <= n & n <= len f holds
f . n >= 1 ) by FINSEQ_3:25; :: thesis: ( ( for n being Nat st 1 <= n & n <= len f holds
f . n >= 1 ) implies f is with_values_greater_or_equal_one )
assume A1: for n being Nat st 1 <= n & n <= len f holds
f . n >= 1 ; :: thesis: f is with_values_greater_or_equal_one
let x be object ; :: according to NUMBER13:def 3 :: thesis: ( x in dom f implies f . x >= 1 )
assume A2: x in dom f ; :: thesis: f . x >= 1
then reconsider x = x as Element of NAT ;
( 1 <= x & x <= len f ) by A2, FINSEQ_3:25;
hence f . x >= 1 by A1; :: thesis: verum