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