set P = F ';' G;
let f, n be Nat; :: according to AFINSQ_1:def 12 :: thesis: ( not n in proj1 (F ';' G) or n <= f or f in proj1 (F ';' G) )
assume that
A1: n in dom (F ';' G) and
A2: f < n ; :: thesis: f in proj1 (F ';' G)
set k = (card F) -' 1;
A3: dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Reloc (G,((card F) -' 1)))) by FUNCT_4:def 1;

per cases ( n in dom (CutLastLoc F) or n in dom (Reloc (G,((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, AFINSQ_1:def 12;
hence f in proj1 (F ';' G) by A3, XBOOLE_0:def 3; :: thesis: verum

end;

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

then n in { (w + ((card F) -' 1)) where w is Nat : w in dom (IncAddr (G,((card F) -' 1))) } by VALUED_1:def 12;
then consider m being Nat such that
A4: n = m + ((card F) -' 1) and
A5: m in dom (IncAddr (G,((card F) -' 1))) ;
A6: m in dom G by A5, Def9;

now :: thesis: ( ( f < (card F) -' 1 & f in dom (CutLastLoc F) ) or ( f >= (card F) -' 1 & f in dom (Reloc (G,((card F) -' 1))) ) )

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

case A7: f < (card F) -' 1 ; :: thesis: f in dom (CutLastLoc F)

then f < (card F) - 1 by PRE_CIRC:20;
then 1 + f < 1 + ((card F) - 1) by XREAL_1:6;
then A8: 1 + f in dom F by AFINSQ_1:66;
f < 1 + f by NAT_1:19;
then A9: f in dom F by A8, AFINSQ_1:def 12;
f <> LastLoc F by A7, AFINSQ_1:70;
then not f in {(LastLoc F)} by TARSKI:def 1;
then f in (dom F) \ {(LastLoc F)} by A9, XBOOLE_0:def 5;
hence f in dom (CutLastLoc F) by VALUED_1:36; :: thesis: verum

end;

case f >= (card F) -' 1 ; :: thesis: f in dom (Reloc (G,((card F) -' 1)))

then consider l1 being Nat such that
A10: f = ((card F) -' 1) + l1 by NAT_1:10;
reconsider l1 = l1 as Element of NAT by ORDINAL1:def 12;
A11: dom (Reloc (G,((card F) -' 1))) = { (w + ((card F) -' 1)) where w is Nat : w in dom (IncAddr (G,((card F) -' 1))) } by VALUED_1:def 12;
( l1 < m or l1 = m ) by A10, A4, A2, XREAL_1:6;
then l1 in dom G by A6, AFINSQ_1:def 12;
then l1 in dom (IncAddr (G,((card F) -' 1))) by Def9;
hence f in dom (Reloc (G,((card F) -' 1))) by A11, A10; :: thesis: verum

end;

end;

end;

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

end;

end;