let a be Int_position; :: thesis: for l being Nat holds not a in dom (Start-At (l,SCMPDS))

let l be Nat; :: thesis: not a in dom (Start-At (l,SCMPDS))

A1: dom (Start-At (l,SCMPDS)) = {(IC )} by FUNCOP_1:13;

assume a in dom (Start-At (l,SCMPDS)) ; :: thesis: contradiction

then a = IC by A1, TARSKI:def 1;

hence contradiction by SCMPDS_2:43; :: thesis: verum

let l be Nat; :: thesis: not a in dom (Start-At (l,SCMPDS))

A1: dom (Start-At (l,SCMPDS)) = {(IC )} by FUNCOP_1:13;

assume a in dom (Start-At (l,SCMPDS)) ; :: thesis: contradiction

then a = IC by A1, TARSKI:def 1;

hence contradiction by SCMPDS_2:43; :: thesis: verum