let I, J be Program of ; :: 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:13;
dom (I +* (I ';' J)) = (dom I) \/ (dom (I ';' J)) by FUNCT_4:def 1
.= dom (I ';' J) by Th56, XBOOLE_1:12 ;
hence I +* (I ';' J) = I ';' J by A1, FUNCT_1:2; :: thesis: verum