let m be Nat; :: thesis: rng (constF m) c= PrimRec
set f = constF m;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (constF m) or y in PrimRec )
assume y in rng (constF m) ; :: thesis: y in PrimRec
then consider x being Element of NAT such that
A1: (constF m) . x = y by FUNCT_2:113;
(constF m) . x = m const x by Def16;
hence y in PrimRec by A1, COMPUT_1:69; :: thesis: verum