dom m = A by Th20;
then A1: m . a in rng m by FUNCT_1:def 3;
rng m c= NAT by Th20, MONOID_0:46;
hence m . a is Element of NAT by A1; :: thesis: verum