let G be non empty 1-sorted ; :: thesis: ((SCM-VAL G) * SCM-OK) . NAT = NAT
A1: NAT in SCM-Memory by AMI_2:22;
then NAT in dom SCM-OK by PARTFUN1:def 2;
then A2: ((SCM-VAL G) * SCM-OK) . NAT = (SCM-VAL G) . (SCM-OK . NAT) by FUNCT_1:13;
((SCM-VAL G) * SCM-OK) . NAT = (SCM-VAL G) . 0 by A2, A1, AMI_2:def 4;
hence ((SCM-VAL G) * SCM-OK) . NAT = NAT ; :: thesis: verum