let s, ss be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA holds DataPart (ss +* (s | NAT)) = DataPart ss
set D = Int-Locations \/ FinSeq-Locations;
let I be Program of SCM+FSA; :: thesis: DataPart (ss +* (s | NAT)) = DataPart ss
A1: NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
dom (ProgramPart s) = NAT by COMPOS_1:34;
hence DataPart (ss +* (s | NAT)) = DataPart ss by A1, FUNCT_4:76, SCMFSA_2:127; :: thesis: verum