let s be State of SCM+FSA; :: thesis: for P being preProgram of SCM+FSA holds DataPart (s +* P) = DataPart s
set D = Int-Locations \/ FinSeq-Locations;
set A = NAT ;
let P be preProgram of SCM+FSA; :: thesis: DataPart (s +* P) = DataPart s
A1: NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
dom P c= NAT by RELAT_1:def 18;
then dom P misses Int-Locations \/ FinSeq-Locations by A1, XBOOLE_1:63;
hence DataPart (s +* P) = DataPart s by FUNCT_4:76, SCMFSA_2:127; :: thesis: verum