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