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