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