let I, J be Program of SCMPDS ; :: thesis: for l being Element of NAT st l in dom J holds
(I ';' J) . (l + (card I)) = J . l
let l be Element of NAT ; :: 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 ;
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