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 ((F ';' G) /. f),f c= proj1 (F ';' G) )
assume A1: f in dom (F ';' G) ; :: thesis: NIC ((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)) = { (m + ((card F) -' 1)) where m is Element of NAT : m in dom (IncAddr G,((card F) -' 1)) } by VALUED_1:def 12;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in NIC ((F ';' G) /. f),f or x in proj1 (F ';' G) )
assume x in NIC ((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 = (F ';' G) /. f ;
A9: (F ';' G) /. f = (F ';' G) . f by A1, PARTFUN1:def 8;

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 (F /. f),f c= dom F by A4, AMISTD_1:def 17;
X: (ProgramPart s2) /. f = s2 . f by COMPOS_1:38;
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, X, FUNCT_4:12
.= F . f by A10, GRFUNC_1:8
.= F /. f by A4, A10, PARTFUN1:def 8 ;
then IC (Following (ProgramPart s2),s2) in NIC (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 = m + ((card F) -' 1) and
A15: m in dom (IncAddr G,((card F) -' 1)) by A5;
A16: m in dom G by A15, Def15;
then A17: NIC (G /. m),m c= dom G by AMISTD_1:def 17;
A18: ObjectKind (IC S) = NAT by COMPOS_1:def 6;
reconsider v = (IC S) .--> m as FinPartState of S by A18, COMPOS_1:5;
set s1 = s2 +* v;
A19: (F ';' G) /. f = (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) . f by A9, A13, FUNCT_4:14
.= (IncAddr G,((card F) -' 1)) . m by A14, A15, VALUED_1:def 12 ;
A20: ((IC S) .--> m) . (IC S) = m by FUNCOP_1:87;
A21: IC S in {(IC S)} by TARSKI:def 1;
A22: dom ((IC S) .--> m) = {(IC S)} by FUNCOP_1:19;
reconsider w = (IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1)) as FinPartState of S by A18, COMPOS_1:5;
(s2 +* v) +* w is State of S ;
then A24: dom ((s2 +* v) +* ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) = 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)))) . a

proof

let a be set ; :: thesis: ( a in dom s2 implies s2 . a = ((s2 +* v) +* ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) . a )
assume a in dom s2 ; :: thesis: s2 . a = ((s2 +* v) +* ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) . a
A25: dom ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1))) = {(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)))) . a

hence s2 . a = (IC (s2 +* v)) + ((card F) -' 1) by A7, A14, A22, A20, A21, FUNCT_4:14
.= ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1))) . a by A26, FUNCOP_1:87
.= ((s2 +* v) +* ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) . 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)))) . a

then A28: not a in dom ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1))) by A25, TARSKI:def 1;
not a in dom ((IC 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)))) . a by A28, FUNCT_4:12; :: thesis: verum

end;

end;

end;

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

now

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

end;

then A32: IC ((s2 +* v) +* (m .--> (G /. m))) = (s2 +* v) . (IC S) by FUNCT_4:12
.= m by A20, A21, A22, FUNCT_4:14 ;
A33: ((s2 +* v) +* (m .--> (G /. m))) . m = (m .--> (G /. m)) . m by A31, FUNCT_4:14
.= G /. m by FUNCOP_1:87 ;
X: (ProgramPart ((s2 +* v) +* (m .--> (G /. m)))) /. m = ((s2 +* v) +* (m .--> (G /. m))) . m by COMPOS_1:38;
A34: dom (s2 +* v) = the carrier of S by PARTFUN1:def 4;
A35: dom ((s2 +* v) +* (m .--> (G /. 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) +* (m .--> (G /. m))) . x

proof

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

end;

then (s2 +* v) | ((dom (s2 +* v)) \ NAT ) = ((s2 +* v) +* (m .--> (G /. m))) | ((dom ((s2 +* v) +* (m .--> (G /. m)))) \ NAT ) by A34, A35, FUNCT_1:165;
then s2 +* v,(s2 +* v) +* (m .--> (G /. m)) equal_outside NAT by FUNCT_7:def 2;
then A37: Exec (G /. m),(s2 +* v), Exec (G /. m),((s2 +* v) +* (m .--> (G /. m))) equal_outside NAT by Def19;
reconsider s3 = (s2 +* v) +* (m .--> (G /. 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 (G /. m),k),s2) by A6, A7, A8, A16, A19, Def15
.= (IC (Exec (G /. m),(s2 +* v))) + k by A29, Def17
.= (IC (Exec (G /. m),s3)) + k by A37, COMPOS_1:24 ;
IC (Following (ProgramPart s3),s3) = IC (Exec (G /. m),s3) by A32, A33, COMPOS_1:38;
then IC (Exec (G /. m),s3) in NIC (G /. m),m by A32, A33, X;
then IC (Exec (G /. m),s3) in dom G by A17;
then IC (Exec (G /. m),s3) 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;