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)) = { (m + ((card F) -' 1)) where m is Element of 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: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 COMPOS_1:def 26 :: 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 = m + ((card F) -' 1) and
A11: m in dom (IncAddr G,((card F) -' 1)) by A2;
A12: m in dom G by A11, Def15;
then A13: G /. m = G . m by PARTFUN1:def 8;
IncAddr (G /. m),((card F) -' 1) = (IncAddr G,((card F) -' 1)) . m by A12, Def15
.= (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) . (m + ((card F) -' 1)) by A11, VALUED_1:def 12
.= halt S by A5, A9, A10, FUNCT_4:14 ;
then m = LastLoc G by A12, A13, Th35, COMPOS_1:def 26
.= (card G) -' 1 by AFINSQ_1:74 ;
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, AFINSQ_1:74; :: thesis: verum

end;

end;