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

now

let x be set ; :: thesis: ( x in dom (I +* (Start-At l,SCMPDS )) implies not b₁ in SCM-Data-Loc )
assume x in dom (I +* (Start-At l,SCMPDS )) ; :: thesis: not b₁ in SCM-Data-Loc
then x in (dom I) \/ (dom (Start-At l,SCMPDS )) by FUNCT_4:def 1;
then ( x in dom I or x in dom (Start-At l,SCMPDS ) ) by XBOOLE_0:def 3;
then A1: ( x in dom I or x in {(IC SCMPDS )} ) by FUNCOP_1:19;

per cases ( x in dom I or x = IC SCMPDS ) by A1, TARSKI:def 1;

suppose A2: x in dom I ; :: thesis: not b₁ in SCM-Data-Loc

dom I c= NAT by RELAT_1:def 18;
hence not x in SCM-Data-Loc by A2, AMI_2:29, XBOOLE_0:3; :: thesis: verum

end;

suppose x = IC SCMPDS ; :: thesis: not b₁ in SCM-Data-Loc

hence not x in SCM-Data-Loc by SCMPDS_3:6; :: thesis: verum

end;

end;

end;

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