let I, J be Program of ; :: thesis: dom I c= dom (I ";" J)
A1: (card (stop I)) -' 1 = card I by COMPOS_1:71;
card (stop (Directed I)) = card (stop I) by Lm2;
then dom (I ";" J) = (dom (Directed I)) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:def 1, A1
.= (dom I) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:99 ;
hence dom I c= dom (I ";" J) by XBOOLE_1:7; :: thesis: verum