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