dom SCMPDS-OK = SCM-Memory by FUNCT_2:def 1;
hence pi ((product SCMPDS-OK),NAT) = SCMPDS-OK . NAT by AMI_2:22, CARD_3:12
.= NAT by Def4, AMI_2:22 ;
:: thesis: verum