let n be Nat; :: thesis: for I, J being Program of st n in dom (Reloc (J,(card I))) holds
(I ";" J) . n = (Reloc (J,(card I))) . n
let I, J be Program of ; :: thesis: ( n in dom (Reloc (J,(card I))) implies (I ";" J) . n = (Reloc (J,(card I))) . n )
assume A1: n in dom (Reloc (J,(card I))) ; :: thesis: (I ";" J) . n = (Reloc (J,(card I))) . n
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 (I ";" J) . n = (Reloc (J,(card I))) . n by A1, FUNCT_4:13; :: thesis: verum