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:30, CARD_3:22
.= NAT by Def3, AMI_2:30 ;
:: thesis: verum