let I, J be Program of SCMPDS ; :: thesis: (Initialize (stop I)) +* (Initialize (stop (I ';' J))) = Initialize (stop (I ';' J))
set sI = stop I;
set IsI = Initialize (stop I);
set sIJ = stop (I ';' J);
set IsIJ = Initialize (stop (I ';' J));
A1: dom (Initialize (stop I)) = (dom (stop I)) \/ {(IC SCMPDS )} by COMPOS_1:76;
A2: dom (Initialize (stop (I ';' J))) = (dom (stop (I ';' J))) \/ {(IC SCMPDS )} by COMPOS_1:76;
dom (stop I) c= dom (stop (I ';' J)) by Th16;
hence (Initialize (stop I)) +* (Initialize (stop (I ';' J))) = Initialize (stop (I ';' J)) by A1, A2, FUNCT_4:20, XBOOLE_1:9; :: thesis: verum