set P = F ';' G;
set k = (card F) -' 1;
A1: dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Reloc (G,((card F) -' 1)))) by FUNCT_4:def 1;
A2: 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;
A3: (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 A4: (((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 A3, XREAL_0:def 2 ;
let f be Nat; :: according to COMPOS_1:def 15 :: thesis: ( (F ';' G) . f = halt S & f in dom (F ';' G) implies f = LastLoc (F ';' G) )
assume that
A5: (F ';' G) . f = halt S and
A6: f in dom (F ';' G) ; :: thesis: f = LastLoc (F ';' G)

per cases ( f in dom (CutLastLoc F) or f in dom (Reloc (G,((card F) -' 1))) ) by A1, A6, XBOOLE_0:def 3;

suppose A7: f in dom (CutLastLoc F) ; :: thesis: f = LastLoc (F ';' G)

then A8: (CutLastLoc F) . f <> halt S by Th10;
dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1))) by Th9;
then CutLastLoc F c= F ';' G by FUNCT_4:32;
hence f = LastLoc (F ';' G) by A5, A7, A8, GRFUNC_1:2; :: thesis: verum

end;

suppose A9: f in dom (Reloc (G,((card F) -' 1))) ; :: thesis: f = LastLoc (F ';' G)

then consider m being Nat such that
A10: f = m + ((card F) -' 1) and
A11: m in dom (IncAddr (G,((card F) -' 1))) by A2;
A12: m in dom G by A11, Def9;
then A13: G /. m = G . m by PARTFUN1:def 6;
IncAddr ((G /. m),((card F) -' 1)) = (IncAddr (G,((card F) -' 1))) . m by A12, Def9
.= (Reloc (G,((card F) -' 1))) . (m + ((card F) -' 1)) by A11, VALUED_1:def 12
.= halt S by A5, A9, A10, FUNCT_4:13 ;
then G . m = halt S by A13, COMPOS_0:12;
then m = LastLoc G by A12, Def7
.= (card G) -' 1 by AFINSQ_1:70 ;
then m + ((card F) -' 1) = (((card F) + (card G)) -' 1) -' 1 by A4, NAT_1:14, NAT_D:38
.= (card (F ';' G)) -' 1 by Th11 ;
hence f = LastLoc (F ';' G) by A10, AFINSQ_1:70; :: thesis: verum

end;

end;