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