let n be Nat; :: thesis: for f, g being real-valued Function st rng g c= rng f & f <= n holds
g <= n
let f, g be real-valued Function; :: thesis: ( rng g c= rng f & f <= n implies g <= n )
assume that
A1: rng g c= rng f and
A2: f <= n ; :: thesis: g <= n
let x be object ; :: according to NUMBER08:def 4 :: thesis: ( x in dom g implies g . x <= n )
assume x in dom g ; :: thesis: g . x <= n
then g . x in rng g by FUNCT_1:def 3;
then ex a being object st
( a in dom f & f . a = g . x ) by A1, FUNCT_1:def 3;
hence g . x <= n by A2; :: thesis: verum