A1: NAT in dom SCM-OK by AMI_2:22, FUNCT_2:def 1;
thus SCM+FSA-OK . NAT = ((SCM+FSA-Memory --> (INT *)) +* SCM-OK) . NAT
.= SCM-OK . NAT by A1, FUNCT_4:13
.= NAT by AMI_2:6, AMI_2:22 ; :: thesis: verum