let I, J be Program of SCMPDS; :: thesis: Shift ((stop J),(card I)) c= stop (I ';' J)
stop (I ';' J) = (I ';' J) ';' (Stop SCMPDS)
.= I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:30
.= I ';' (stop J) ;
then stop (I ';' J) = I +* (Shift ((stop J),(card I))) ;
hence Shift ((stop J),(card I)) c= stop (I ';' J) by FUNCT_4:26; :: thesis: verum