hereby :: thesis: ( ( for x being object st x in dom f holds
f . x >= 1 ) implies f is with_values_greater_or_equal_one )

assume A1: f is with_values_greater_or_equal_one ; :: thesis: for x being object st x in dom f holds
f . x >= 1
let x be object ; :: thesis: ( x in dom f implies f . x >= 1 )
assume x in dom f ; :: thesis: f . x >= 1
then f . x in rng f by FUNCT_1:def 3;
hence f . x >= 1 by A1; :: thesis: verum

end;

assume A2: for x being object st x in dom f holds
f . x >= 1 ; :: thesis: f is with_values_greater_or_equal_one
let r be ExtReal; :: according to NUMBER13:def 2 :: thesis: ( r in rng f implies r >= 1 )
assume r in rng f ; :: thesis: r >= 1
then ex x being object st
( x in dom f & f . x = r ) by FUNCT_1:def 3;
hence r >= 1 by A2; :: thesis: verum