set P = F ';' G;
let n be Element of NAT ; :: according to AMISTD_1:def 20 :: thesis: ( not n in proj1 (F ';' G) or for b₁ being Element of NAT holds
( not b₁ <= n,S or b₁ in proj1 (F ';' G) ) )
assume A1: n in dom (F ';' G) ; :: thesis: for b₁ being Element of NAT holds
( not b₁ <= n,S or b₁ in proj1 (F ';' G) )
let f be Element of NAT ; :: thesis: ( not f <= n,S or f in proj1 (F ';' G) )
assume A2: f <= n,S ; :: thesis: f in proj1 (F ';' G)
set k = (card F) -' 1;
A3: dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) by FUNCT_4:def 1;

per cases ( n in dom (CutLastLoc F) or n in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) ) by A1, A3, XBOOLE_0:def 3;

suppose n in dom (CutLastLoc F) ; :: thesis: f in proj1 (F ';' G)

then f in dom (CutLastLoc F) by A2, AMISTD_1:def 20;
hence f in proj1 (F ';' G) by A3, XBOOLE_0:def 3; :: thesis: verum

end;

suppose n in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) ; :: thesis: f in proj1 (F ';' G)

then n in { (il. S,(w + ((card F) -' 1))) where w is Element of NAT : il. S,w in dom (IncAddr G,((card F) -' 1)) } by Def16;
then consider m being Element of NAT such that
A4: n = il. S,(m + ((card F) -' 1)) and
A5: il. S,m in dom (IncAddr G,((card F) -' 1)) ;
A6: locnum f,S <= locnum n,S by A2, AMISTD_1:29;
A7: il. S,m in dom G by A5, Def15;

now

per cases ( locnum f,S < (card F) -' 1 or locnum f,S >= (card F) -' 1 ) ;

case A8: locnum f,S < (card F) -' 1 ; :: thesis: f in dom (CutLastLoc F)

then locnum f,S < (card F) - 1 by PRE_CIRC:25;
then 1 + (locnum f,S) < 1 + ((card F) - 1) by XREAL_1:8;
then A9: il. S,(1 + (locnum f,S)) in dom F by AMISTD_1:50;
locnum f,S <= 1 + (locnum f,S) by NAT_1:11;
then il. S,(locnum f,S) <= il. S,(1 + (locnum f,S)),S by AMISTD_1:28;
then il. S,(locnum f,S) in dom F by A9, AMISTD_1:def 20;
then A10: f in dom F by AMISTD_1:def 13;

now

assume f = LastLoc F ; :: thesis: contradiction
then f = il. S,((card F) -' 1) by AMISTD_1:55;
hence contradiction by A8, AMISTD_1:def 13; :: thesis: verum

end;

then not f in {(LastLoc F)} by TARSKI:def 1;
then f in (dom F) \ {(LastLoc F)} by A10, XBOOLE_0:def 5;
hence f in dom (CutLastLoc F) by Th47; :: thesis: verum

end;

case locnum f,S >= (card F) -' 1 ; :: thesis: f in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))

then consider l1 being Nat such that
A11: locnum f,S = ((card F) -' 1) + l1 by NAT_1:10;
reconsider l1 = l1 as Element of NAT by ORDINAL1:def 13;
A12: dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) = { (il. S,(w + ((card F) -' 1))) where w is Element of NAT : il. S,w in dom (IncAddr G,((card F) -' 1)) } by Def16;
A13: f = il. S,(l1 + ((card F) -' 1)) by A11, AMISTD_1:def 13;
locnum f,S <= ((card F) -' 1) + m by A4, A6, AMISTD_1:def 13;
then l1 <= m by A11, XREAL_1:8;
then il. S,l1 <= il. S,m,S by AMISTD_1:28;
then il. S,l1 in dom G by A7, AMISTD_1:def 20;
then il. S,l1 in dom (IncAddr G,((card F) -' 1)) by Def15;
hence f in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) by A12, A13; :: thesis: verum

end;

end;

end;

hence f in proj1 (F ';' G) by A3, XBOOLE_0:def 3; :: thesis: verum

end;

end;