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