let I be Program of SCMPDS ; :: thesis: for a being Int_position
for l being Element of NAT holds not a in dom (I +* (Start-At l,SCMPDS ))
let a be Int_position ; :: thesis: for l being Element of NAT holds not a in dom (I +* (Start-At l,SCMPDS ))
let l be Element of NAT ; :: thesis: not a in dom (I +* (Start-At l,SCMPDS ))
assume a in dom (I +* (Start-At l,SCMPDS )) ; :: thesis: contradiction
then a in (dom I) \/ (dom (Start-At l,SCMPDS )) by FUNCT_4:def 1;
then A1: ( a in dom I or a in dom (Start-At l,SCMPDS ) ) by XBOOLE_0:def 3;
( dom I c= NAT & a in SCM-Data-Loc ) by SCMPDS_2:def 2;
hence contradiction by A1, Th59, AMI_2:29, XBOOLE_0:3; :: thesis: verum