let n be Element of NAT ; :: thesis: for I being Program of st card I > 0 holds
(Shift (stop I),n) . (inspos n) = (Shift I,n) . (inspos n)
let I be Program of ; :: thesis: ( card I > 0 implies (Shift (stop I),n) . (inspos n) = (Shift I,n) . (inspos n) )
assume card I > 0 ; :: thesis: (Shift (stop I),n) . (inspos n) = (Shift I,n) . (inspos n)
then A1: inspos 0 in dom I by SCMPDS_4:1;
thus (Shift (stop I),n) . (inspos n) = (Shift (stop I),n) . (inspos (0 + n))
.= (Shift (stop I),n) . ((inspos 0 ) + n)
.= (Shift I,n) . ((inspos 0 ) + n) by A1, Th18
.= (Shift I,n) . (inspos (0 + n))
.= (Shift I,n) . (inspos n) ; :: thesis: verum