set P = F ';' G;
set k = (card F) -' 1;
A1:
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;
A2:
(card G) -' 1 = LastLoc G
by AFINSQ_1:70;
then A3:
(card G) -' 1 in dom G
by VALUED_1:30;
then A4:
(card G) -' 1 in dom (IncAddr (G,((card F) -' 1)))
by Def9;
then A5:
((card F) -' 1) + ((card G) -' 1) in dom (Reloc (G,((card F) -' 1)))
by A1;
A6: G /. ((card G) -' 1) =
G . ((card G) -' 1)
by A2, PARTFUN1:def 6, VALUED_1:30
.=
halt S
by A2, Def6
;
A7:
(card G) - 1 >= 0
by NAT_1:14, XREAL_1:48;
then
((card F) -' 1) + ((card G) - 1) >= ((card F) -' 1) + 0
by XREAL_1:6;
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) . ((card (F ';' G)) -' 1)
by AFINSQ_1:70
.=
(F ';' G) . ((((card F) + (card G)) -' 1) -' 1)
by Th11
.=
(F ';' G) . ((((card F) -' 1) + (card G)) -' 1)
by NAT_1:14, NAT_D:38
.=
(Reloc (G,((card F) -' 1))) . (((card F) -' 1) + ((card G) -' 1))
by A5, A8, FUNCT_4:13
.=
(IncAddr (G,((card F) -' 1))) . ((card G) -' 1)
by A4, VALUED_1:def 12
.=
IncAddr ((G /. ((card G) -' 1)),((card F) -' 1))
by A3, Def9
.=
halt S
by A6, COMPOS_0:4
; COMPOS_1:def 14 verum