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 COMPOS_1:50;
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 3
.= (Load i) . 0 by A1, AFINSQ_1:def 3
.= i ; :: thesis: card I in dom (I ';' i)
card (I ';' i) = (card I) + 1 by Th4;
then card I < card (I ';' i) by XREAL_1:29;
hence card I in dom (I ';' i) by AFINSQ_1:66; :: thesis: verum