set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
let s be State of SCM+FSA ; :: thesis: for P being preProgram of SCM+FSA holds DataPart (s +* P) = DataPart s
let P be preProgram of SCM+FSA ; :: thesis: DataPart (s +* P) = DataPart s
A1: dom P c= NAT by RELAT_1:def 18;
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
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