let I, J be Program of ; :: thesis: I +* (I ";" J) = I ";" J
A1: for x being object 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 Th7, XBOOLE_1:12 ;
hence I +* (I ";" J) = I ";" J by A1, FUNCT_1:2; :: thesis: verum