set P = F ';' G;
set k = (card F) -' 1;
A1: dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) = { (il. S,(m + ((card F) -' 1))) where m is Element of NAT : il. S,m in dom (IncAddr G,((card F) -' 1)) } by Def16;
A2: il. S,((card G) -' 1) = LastLoc G by AMISTD_1:55;
then A3: il. S,((card G) -' 1) in dom G by AMISTD_1:51;
then A4: il. S,((card G) -' 1) in dom (IncAddr G,((card F) -' 1)) by Def15;
then A5: il. S,(((card F) -' 1) + ((card G) -' 1)) in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) by A1;
A6: pi G,(il. S,((card G) -' 1)) = G . (il. S,((card G) -' 1)) by A3, AMI_1:def 47
.= halt S by A2, AMISTD_1:def 22 ;
A7: (card G) - 1 >= 0 by NAT_1:14, XREAL_1:50;
then ((card F) -' 1) + ((card G) - 1) >= ((card F) -' 1) + 0 by XREAL_1:8;
then A8: (((card F) -' 1) + (card G)) -' 1 = (((card F) -' 1) + (card G)) - 1 by XREAL_0:def 2
.= ((card F) -' 1) + ((card G) - 1)
.= ((card F) -' 1) + ((card G) -' 1) by A7, XREAL_0:def 2 ;
thus (F ';' G) . (LastLoc (F ';' G)) = (F ';' G) . (il. S,((card (F ';' G)) -' 1)) by AMISTD_1:55
.= (F ';' G) . (il. S,((((card F) + (card G)) -' 1) -' 1)) by Th52
.= (F ';' G) . (il. S,((((card F) -' 1) + (card G)) -' 1)) by NAT_1:14, NAT_D:38
.= (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) . (il. S,(((card F) -' 1) + ((card G) -' 1))) by A5, A8, FUNCT_4:14
.= (IncAddr G,((card F) -' 1)) . (il. S,((card G) -' 1)) by A4, Def16
.= IncAddr (pi G,(il. S,((card G) -' 1))),((card F) -' 1) by A3, Def15
.= halt S by A6, Th29 ; :: according to AMISTD_1:def 22 :: thesis: verum