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 AFINSQ_1:70;
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