A1: NAT in dom SCM-OK by AMI_2:30, FUNCT_2:def 1;
not NAT in dom ((SCM-Instr .--> SCM+FSA-Instr) * (SCM-OK | NAT)) by Lm1;
hence SCM+FSA-OK . NAT = ((SCM+FSA-Memory --> (INT *)) +* SCM-OK) . NAT by FUNCT_4:12
.= SCM-OK . NAT by A1, FUNCT_4:14
.= NAT by AMI_2:7, AMI_2:30 ;
:: thesis: verum