let I, J be Program of ; :: thesis: (stop I) +* (stop (I ';' J)) = stop (I ';' J)
set sI = stop I;
set IsI = stop I;
set sIJ = stop (I ';' J);
set IsIJ = stop (I ';' J);
dom (stop I) c= dom (stop (I ';' J)) by Th2;
hence (stop I) +* (stop (I ';' J)) = stop (I ';' J) by FUNCT_4:19; :: thesis: verum