let S be COM-Struct ; :: thesis: for F, G being Program of S holds (F ';' G) . (LastLoc F) = (IncAddr (G,((card F) -' 1))) . 0
let F, G be Program of S; :: thesis: (F ';' G) . (LastLoc F) = (IncAddr (G,((card F) -' 1))) . 0
set k = (card F) -' 1;
A1: LastLoc F = 0 + ((card F) -' 1) by AFINSQ_1:70;
A2: 0 in dom (IncAddr (G,((card F) -' 1))) by AFINSQ_1:65;
dom (Reloc (G,((card F) -' 1))) = { (m + ((card F) -' 1)) where m is Nat : m in dom (IncAddr (G,((card F) -' 1))) } by VALUED_1:def 12;
then LastLoc F in dom (Reloc (G,((card F) -' 1))) by A1, A2;
hence (F ';' G) . (LastLoc F) = (Reloc (G,((card F) -' 1))) . (LastLoc F) by FUNCT_4:13
.= (IncAddr (G,((card F) -' 1))) . 0 by A1, A2, VALUED_1:def 12 ;
:: thesis: verum