let I, J be Program of ; :: thesis: dom (I ";" J) = (dom I) \/ (dom (Reloc (J,(card I))))
I ";" J = (CutLastLoc (stop (Directed I))) +* (Reloc (J,((card (stop I)) -' 1))) by Th27
.= (Directed I) +* (Reloc (J,(card I))) by COMPOS_1:71 ;
hence dom (I ";" J) = (dom (Directed I)) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:def 1
.= (dom I) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:99 ;
:: thesis: verum