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

now

let x be set ; :: thesis: ( x in dom (Start-At (l,SCMPDS)) implies not x in SCM-Data-Loc )
assume x in dom (Start-At (l,SCMPDS)) ; :: thesis: not x in SCM-Data-Loc
then x in {(IC SCMPDS)} by FUNCOP_1:19;
hence not x in SCM-Data-Loc by SCMPDS_3:6, TARSKI:def 1; :: thesis: verum

end;

then dom (Start-At (l,SCMPDS)) misses SCM-Data-Loc by XBOOLE_0:3;
hence DataPart s = DataPart (s +* (Start-At (l,SCMPDS))) by FUNCT_4:76, SCMPDS_2:100; :: thesis: verum