dom SCM+FSA-OK = (dom (SCM+FSA-Memory --> 2)) \/ (dom SCM-OK) by FUNCT_4:def 1;
hence dom SCM-OK c= dom SCM+FSA-OK by XBOOLE_1:7; :: thesis: verum