let I, J be Program of ; :: thesis: Shift ((stop J),(card I)) c= stop (I ';' J)
stop (I ';' J) = (I ';' J) ';' (Stop SCMPDS)
.= I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:27
.= 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:25; :: thesis: verum