NAT in dom SCM-OK by Lm3, PARTFUN1:def 2;
then A1: (SCM-VAL * SCM-OK) . NAT = SCM-VAL . (SCM-OK . NAT) by FUNCT_1:13;
(SCM-VAL * SCM-OK) . NAT = SCM-VAL . 0 by A1, Def2, Lm3;
hence (SCM-VAL * SCM-OK) . NAT = NAT ; :: thesis: verum