let I, J, K be Program of SCMPDS ; (I ';' J) ';' K = I ';' (J ';' K)
Shift (J ';' K),(card I) =
(Shift J,(card I)) +* (Shift (Shift K,(card J)),(card I))
by VALUED_1:24
.=
(Shift J,(card I)) +* (Shift K,((card J) + (card I)))
by VALUED_1:22
.=
(Shift J,(card I)) +* (Shift K,(card (I ';' J)))
by Th45
;
hence
(I ';' J) ';' K = I ';' (J ';' K)
by FUNCT_4:15; verum