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