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