set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
let s, ss be State of SCM+FSA ; :: thesis: DataPart (s +* (ss | NAT )) = DataPart s
dom (ss | NAT ) = (dom ss) /\ NAT by RELAT_1:90
.= (((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) /\ NAT by SCMFSA6A:34
.= NAT by XBOOLE_1:21 ;
then dom (ss | NAT ) misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
hence DataPart (s +* (ss | NAT )) = DataPart s by FUNCT_4:76, SCMFSA_2:127; :: thesis: verum