set P = F ';' G;
set k = (card F) -' 1;
let f be Element of NAT ; :: according to AMISTD_1:def 17 :: thesis: ( not f in proj1 (F ';' G) or NIC (pi (F ';' G),f),f c= proj1 (F ';' G) )
assume A1: f in dom (F ';' G) ; :: thesis: NIC (pi (F ';' G),f),f c= proj1 (F ';' G)
A2: dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) by FUNCT_4:def 1;
dom (CutLastLoc F) misses dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) by Th50;
then A3: (dom (CutLastLoc F)) /\ (dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) = {} by XBOOLE_0:def 7;
A4: dom (CutLastLoc F) c= dom F by GRFUNC_1:8;
A5: 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;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in NIC (pi (F ';' G),f),f or x in proj1 (F ';' G) )
assume x in NIC (pi (F ';' G),f),f ; :: thesis: x in proj1 (F ';' G)
then consider s2 being Element of product the Object-Kind of S such that
A6: x = IC (Following (ProgramPart s2),s2) and
A7: IC s2 = f and
A8: (ProgramPart s2) /. f = pi (F ';' G),f ;
A9: pi (F ';' G),f = (F ';' G) . f by A1, AMI_1:def 47;

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

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

then A11: NIC (pi F,f),f c= dom F by A4, AMISTD_1:def 17;
X: (ProgramPart s2) /. f = s2 . f by AMI_1:150;
not f in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) by A3, A10, XBOOLE_0:def 4;
then s2 . f = (CutLastLoc F) . f by A8, A9, FUNCT_4:12, X
.= F . f by A10, GRFUNC_1:8
.= pi F,f by A4, A10, AMI_1:def 47 ;
then IC (Following (ProgramPart s2),s2) in NIC (pi F,f),f by A7, X;
then A12: x in dom F by A6, A11;
dom F c= dom (F ';' G) by Th53;
hence x in proj1 (F ';' G) by A12; :: thesis: verum

end;

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

then consider m being Element of NAT such that
A14: f = il. S,(m + ((card F) -' 1)) and
A15: il. S,m in dom (IncAddr G,((card F) -' 1)) by A5;
A16: il. S,m in dom G by A15, Def15;
then A17: NIC (pi G,(il. S,m)),(il. S,m) c= dom G by AMISTD_1:def 17;
A18: ObjectKind (IC S) = NAT by AMI_1:def 11;
reconsider v = (IC S) .--> (il. S,m) as FinPartState of S by A18, AMI_1:59;
set s1 = s2 +* v;
A19: pi (F ';' G),f = (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) . f by A9, A13, FUNCT_4:14
.= (IncAddr G,((card F) -' 1)) . (il. S,m) by A14, A15, Def16 ;
A20: ((IC S) .--> (il. S,m)) . (IC S) = il. S,m by FUNCOP_1:87;
A21: IC S in {(IC S)} by TARSKI:def 1;
A22: dom ((IC S) .--> (il. S,m)) = {(IC S)} by FUNCOP_1:19;
then A23: IC (s2 +* v) = il. S,m by A20, A21, FUNCT_4:14;
reconsider w = (IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1),S) as FinPartState of S by A18, AMI_1:59;
(s2 +* v) +* w is State of S ;
then A24: dom ((s2 +* v) +* ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1),S))) = the carrier of S by PARTFUN1:def 4;
X: dom s2 = the carrier of S by PARTFUN1:def 4;
for a being set st a in dom s2 holds
s2 . a = ((s2 +* v) +* ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1),S))) . a

proof

let a be set ; :: thesis: ( a in dom s2 implies s2 . a = ((s2 +* v) +* ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1),S))) . a )
assume a in dom s2 ; :: thesis: s2 . a = ((s2 +* v) +* ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1),S))) . a
A25: dom ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1),S)) = {(IC S)} by FUNCOP_1:19;

per cases ( a = IC S or a <> IC S ) ;

suppose A26: a = IC S ; :: thesis: s2 . a = ((s2 +* v) +* ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1),S))) . a

hence s2 . a = il. S,((locnum (IC (s2 +* v)),S) + ((card F) -' 1)) by A7, A14, A23, AMISTD_1:def 13
.= ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1),S)) . a by A26, FUNCOP_1:87
.= ((s2 +* v) +* ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1),S))) . a by A21, A25, A26, FUNCT_4:14 ;
:: thesis: verum

end;

suppose A27: a <> IC S ; :: thesis: s2 . a = ((s2 +* v) +* ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1),S))) . a

then A28: not a in dom ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1),S)) by A25, TARSKI:def 1;
not a in dom ((IC S) .--> (il. S,m)) by A22, A27, TARSKI:def 1;
then (s2 +* v) . a = s2 . a by FUNCT_4:12;
hence s2 . a = ((s2 +* v) +* ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1),S))) . a by A28, FUNCT_4:12; :: thesis: verum

end;

end;

end;

then A29: s2 = (s2 +* v) +* ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1),S)) by A24, FUNCT_1:9, X;
set s3 = (s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)));
A30: dom ((il. S,m) .--> (pi G,(il. S,m))) = {(il. S,m)} by FUNCOP_1:19;
then A31: il. S,m in dom ((il. S,m) .--> (pi G,(il. S,m))) by TARSKI:def 1;

now

assume IC S in dom ((il. S,m) .--> (pi G,(il. S,m))) ; :: thesis: contradiction
then reconsider l = IC S as Element of NAT by A30, TARSKI:def 1;
l = IC S ;
hence contradiction by AMI_1:48; :: thesis: verum

end;

then A32: IC ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) = (s2 +* v) . (IC S) by FUNCT_4:12
.= il. S,m by A20, A21, A22, FUNCT_4:14 ;
A33: ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) . (il. S,m) = ((il. S,m) .--> (pi G,(il. S,m))) . (il. S,m) by A31, FUNCT_4:14
.= pi G,(il. S,m) by FUNCOP_1:87 ;
X: (ProgramPart ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m))))) /. (il. S,m) = ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) . (il. S,m) by AMI_1:150;
A34: dom (s2 +* v) = the carrier of S by PARTFUN1:def 4;
A35: dom ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) = the carrier of S by PARTFUN1:def 4;
for x being set st x in (dom (s2 +* v)) \ NAT holds
(s2 +* v) . x = ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) . x

proof

let x be set ; :: thesis: ( x in (dom (s2 +* v)) \ NAT implies (s2 +* v) . x = ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) . x )
A36: dom ((il. S,m) .--> (pi G,(il. S,m))) c= NAT by RELAT_1:def 18;
assume x in (dom (s2 +* v)) \ NAT ; :: thesis: (s2 +* v) . x = ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) . x
then not x in dom ((il. S,m) .--> (pi G,(il. S,m))) by A36, XBOOLE_0:def 5;
hence (s2 +* v) . x = ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) . x by FUNCT_4:12; :: thesis: verum

end;

then (s2 +* v) | ((dom (s2 +* v)) \ NAT ) = ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) | ((dom ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m))))) \ NAT ) by A34, A35, FUNCT_1:165;
then s2 +* v,(s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m))) equal_outside NAT by FUNCT_7:def 2;
then A37: Exec (pi G,(il. S,m)),(s2 +* v), Exec (pi G,(il. S,m)),((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) equal_outside NAT by Def19;
reconsider s3 = (s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m))) as Element of product the Object-Kind of S by PBOOLE:155;
reconsider k = (card F) -' 1, m = m as Element of NAT ;
A38: x = IC (Exec (IncAddr (pi G,(il. S,m)),k),s2) by A6, A7, A8, A16, A19, Def15
.= (IC (Exec (pi G,(il. S,m)),(s2 +* v))) + k,S by A29, Def17
.= il. S,((locnum (IC (Exec (pi G,(il. S,m)),s3)),S) + k) by A37, AMI_1:121 ;
IC (Following (ProgramPart s3),s3) = il. S,(locnum (IC (Exec (pi G,(il. S,m)),s3)),S) by A32, A33, AMISTD_1:def 13, X;
then il. S,(locnum (IC (Exec (pi G,(il. S,m)),s3)),S) in NIC (pi G,(il. S,m)),(il. S,m) by A32, A33, X;
then il. S,(locnum (IC (Exec (pi G,(il. S,m)),s3)),S) in dom G by A17;
then il. S,(locnum (IC (Exec (pi G,(il. S,m)),s3)),S) in dom (IncAddr G,k) by Def15;
then x in dom (Shift (IncAddr G,k),k) by A5, A38;
hence x in proj1 (F ';' G) by A2, XBOOLE_0:def 3; :: thesis: verum

end;

end;