reconsider z = NAT as Element of SCM+FSA-Memory by Th2;
dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then pi ((product (SCM*-VAL * SCM+FSA-OK)),NAT) = (SCM*-VAL * SCM+FSA-OK) . z by CARD_3:12
.= NAT by Th4 ;
hence s . NAT is Element of NAT by CARD_3:def 6; :: thesis: verum