let J, I, K be Program of SCMPDS; :: thesis: Shift (J,(card I)) c= (I ';' J) ';' K
set IJ = I ';' J;
dom (I ';' J) misses dom (Shift (K,(card (I ';' J)))) by AFINSQ_1:76;
then A1: I ';' J c= (I ';' J) ';' K by FUNCT_4:33;
Shift (J,(card I)) c= I ';' J by FUNCT_4:26;
hence Shift (J,(card I)) c= (I ';' J) ';' K by A1, XBOOLE_1:1; :: thesis: verum