A1: NAT in dom SCM-OK by AMI_2:22, FUNCT_2:def 1;
dom SCM-OK c= dom SCM+FSA-OK by Lm2;
hence NAT in dom SCM+FSA-OK by A1; :: thesis: verum