let i be Instruction of SCMPDS ; :: thesis: for I being Program of SCMPDS holds
( (I ';' i) . (card I) = i & card I in dom (I ';' i) )
let I be Program of SCMPDS ; :: thesis: ( (I ';' i) . (card I) = i & card I in dom (I ';' i) )
A1: 0 in dom (Load i) by SCMPDS_5:2;
thus (I ';' i) . (card I) = (I ';' i) . (0 + (card I))
.= (I ';' i) . (0 + (card I))
.= (I ';' (Load i)) . (0 + (card I)) by SCMPDS_4:def 5
.= (Load i) . 0 by A1, SCMPDS_4:38
.= i by SCMPDS_5:4 ; :: thesis: 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 card I in dom (I ';' i) by SCMPDS_4:1; :: thesis: verum