let I, J be Program of SCMPDS ; :: thesis: for l being Element of NAT st l in dom I holds
(I ';' J) . l = I . l
let l be Element of NAT ; :: thesis: ( l in dom I implies (I ';' J) . l = I . l )
assume A1: l in dom I ; :: thesis: (I ';' J) . l = I . l

now

assume l in dom (Shift J,(card I)) ; :: thesis: contradiction
then l in { (m + (card I)) where m is Element of NAT : m in dom J } by VALUED_1:def 12;
then consider m being Element of NAT such that
A2: l = m + (card I) and
m in dom J ;
m + (card I) < card I by A1, A2, AFINSQ_1:70;
hence contradiction by NAT_1:11; :: thesis: verum

end;

hence (I ';' J) . l = I . l by FUNCT_4:12; :: thesis: verum