let S be non empty 1-sorted ; :: thesis: dom ((SCM-VAL S) * SCM-OK) = SCM-Memory
A1: dom SCM-OK = SCM-Memory by PARTFUN1:def 2;
len <%NAT, the carrier of S%> = 2 by AFINSQ_1:38;
then rng SCM-OK c= dom (SCM-VAL S) by RELAT_1:def 19;
hence dom ((SCM-VAL S) * SCM-OK) = SCM-Memory by A1, RELAT_1:27; :: thesis: verum