let I, J be Program of ; :: thesis: for l being Instruction-Location of SCMPDS st l in dom J holds
(I ';' J) . (l + (card I)) = J . l
let l be Instruction-Location of SCMPDS ; :: thesis: ( l in dom J implies (I ';' J) . (l + (card I)) = J . l )
assume A1: l in dom J ; :: thesis: (I ';' J) . (l + (card I)) = J . l
reconsider n = l as Element of NAT by ORDINAL1:def 13;
inspos (n + (card I)) in { (m + (card I)) where m is Element of NAT : m in dom J } by A1;
then l + (card I) in dom (Shift J,(card I)) by VALUED_1:def 12;
hence (I ';' J) . (l + (card I)) = (Shift J,(card I)) . (n + (card I)) by FUNCT_4:14
.= J . l by A1, VALUED_1:def 12 ;
:: thesis: verum