reconsider z = NAT as Element of SCM+FSA-Memory by Th5;
dom SCM+FSA-OK = SCM+FSA-Memory by FUNCT_2:def 1;
then pi (product SCM+FSA-OK ),NAT = SCM+FSA-OK . z by CARD_3:22
.= NAT by Th9 ;
hence s . NAT is Element of NAT by CARD_3:def 6; :: thesis: verum