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