let i be Instruction of SCMPDS ; :: thesis: for I being Program of SCMPDS holds
( (I ';' i) . (inspos (card I)) = i & inspos (card I) in dom (I ';' i) )
let I be Program of SCMPDS ; :: thesis: ( (I ';' i) . (inspos (card I)) = i & inspos (card I) in dom (I ';' i) )
A1: inspos 0 in dom (Load i) by SCMPDS_5:2;
thus (I ';' i) . (inspos (card I)) = (I ';' i) . (inspos (0 + (card I)))
.= (I ';' i) . ((inspos 0 ) + (card I))
.= (I ';' (Load i)) . ((inspos 0 ) + (card I)) by SCMPDS_4:def 5
.= (Load i) . (inspos 0 ) by A1, SCMPDS_4:38
.= i by SCMPDS_5:4 ; :: thesis: inspos (card I) in dom (I ';' i)
card (I ';' i) = (card I) + 1 by Th8;
then card I < card (I ';' i) by XREAL_1:31;
hence inspos (card I) in dom (I ';' i) by SCMPDS_4:1; :: thesis: verum