set P = F ';' G;
set k = (card F) -' 1;
A1: dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) by FUNCT_4:def 1;
A2: 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;
A3: (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 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 Element of NAT ; :: according to AMISTD_1:def 23 :: thesis: ( not (F ';' G) . f = halt S or not f in proj1 (F ';' G) or 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 (Shift (IncAddr G,((card F) -' 1)),((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 Th51;
dom (CutLastLoc F) misses dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) by Th50;
then CutLastLoc F c= F ';' G by FUNCT_4:33;
hence f = LastLoc (F ';' G) by A5, A7, A8, GRFUNC_1:8; :: thesis: verum

end;

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

then consider m being Element of NAT such that
A10: f = il. S,(m + ((card F) -' 1)) and
A11: il. S,m in dom (IncAddr G,((card F) -' 1)) by A2;
A12: il. S,m in dom G by A11, Def15;
then A13: pi G,(il. S,m) = G . (il. S,m) by AMI_1:def 47;
IncAddr (pi G,(il. S,m)),((card F) -' 1) = (IncAddr G,((card F) -' 1)) . (il. S,m) by A12, Def15
.= (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) . (il. S,(m + ((card F) -' 1))) by A11, Def16
.= halt S by A5, A9, A10, FUNCT_4:14 ;
then G . (il. S,m) = halt S by A13, Th35;
then il. S,m = LastLoc G by A12, AMISTD_1:def 23
.= il. S,((card G) -' 1) by AMISTD_1:55 ;
then m = (card G) -' 1 by AMISTD_1:25;
then m + ((card F) -' 1) = (((card F) + (card G)) -' 1) -' 1 by A4, NAT_1:14, NAT_D:38
.= (card (F ';' G)) -' 1 by Th52 ;
hence f = LastLoc (F ';' G) by A10, AMISTD_1:55; :: thesis: verum

end;

end;