set P = F ';' G;
set k = (card F) -' 1;
A1:
dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) = { (m + ((card F) -' 1)) where m is Element of NAT : m in dom (IncAddr G,((card F) -' 1)) }
by VALUED_1:def 12;
A2:
(card G) -' 1 = LastLoc G
by AFINSQ_1:74;
then A3:
(card G) -' 1 in dom G
by VALUED_1:31;
then A4:
(card G) -' 1 in dom (IncAddr G,((card F) -' 1))
by Def15;
then A5:
((card F) -' 1) + ((card G) -' 1) in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))
by A1;
A6: G /. ((card G) -' 1) =
G . ((card G) -' 1)
by A2, PARTFUN1:def 8, VALUED_1:31
.=
halt S
by A2, COMPOS_1:def 25
;
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) . ((card (F ';' G)) -' 1)
by AFINSQ_1:74
.=
(F ';' G) . ((((card F) + (card G)) -' 1) -' 1)
by Th52
.=
(F ';' G) . ((((card F) -' 1) + (card G)) -' 1)
by NAT_1:14, NAT_D:38
.=
(Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) . (((card F) -' 1) + ((card G) -' 1))
by A5, A8, FUNCT_4:14
.=
(IncAddr G,((card F) -' 1)) . ((card G) -' 1)
by A4, VALUED_1:def 12
.=
IncAddr (G /. ((card G) -' 1)),((card F) -' 1)
by A3, Def15
.=
halt S
by A6, Th29
; COMPOS_1:def 25 verum