let s be State of SCM+FSA; :: thesis: for l being Element of NAT holds DataPart s = DataPart (s +* (Start-At (l,SCM+FSA)))
let l be Element of NAT ; :: thesis: DataPart s = DataPart (s +* (Start-At (l,SCM+FSA)))

now

let x be set ; :: thesis: ( x in dom (Start-At (l,SCM+FSA)) implies not x in Int-Locations \/ FinSeq-Locations )
assume x in dom (Start-At (l,SCM+FSA)) ; :: thesis: not x in Int-Locations \/ FinSeq-Locations
then x in {(IC SCM+FSA)} by FUNCOP_1:19;
hence not x in Int-Locations \/ FinSeq-Locations by SCMFSA6A:37, TARSKI:def 1; :: thesis: verum

end;

then dom (Start-At (l,SCM+FSA)) misses Int-Locations \/ FinSeq-Locations by XBOOLE_0:3;
hence DataPart s = DataPart (s +* (Start-At (l,SCM+FSA))) by FUNCT_4:76, SCMFSA_2:127; :: thesis: verum