let I, J be Program of SCMPDS ; :: thesis: I +* (I ';' J) = I ';' J
A1: for x being set st x in dom (I ';' J) holds
(I +* (I ';' J)) . x = (I ';' J) . x by FUNCT_4:14;
dom (I +* (I ';' J)) = (dom I) \/ (dom (I ';' J)) by FUNCT_4:def 1
.= dom (I ';' J) by Th39, XBOOLE_1:12 ;
hence I +* (I ';' J) = I ';' J by A1, FUNCT_1:9; :: thesis: verum