let S be non empty 1-sorted ; :: thesis: pi ((product (SCM-OK S)),NAT) = NAT
dom (SCM-OK S) = SCM-Memory by FUNCT_2:def 1;
hence pi ((product (SCM-OK S)),NAT) = (SCM-OK S) . NAT by AMI_2:22, CARD_3:12
.= NAT by Def3, AMI_2:22 ;
:: thesis: verum