let I, J, K be Program of ; :: 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:72;
then A1: I ';' J c= (I ';' J) ';' K by FUNCT_4:32;
Shift (J,(card I)) c= I ';' J by FUNCT_4:25;
hence Shift (J,(card I)) c= (I ';' J) ';' K by A1, XBOOLE_1:1; :: thesis: verum