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;
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 (Exec (((F ';' G) /. f),s2)) and
A7: IC s2 = 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 S: 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;
dom (CutLastLoc F) = (dom F) \ {(LastLoc F)} by VALUED_1:37;
then XX: f in dom F by S, XBOOLE_0:def 5;
dom (CutLastLoc F) misses dom (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1))) by COMPOS_1:100;
then Y: not f in dom (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1))) by S, XBOOLE_0:3;
X: (F ';' G) /. f = (F ';' G) . f by A1, PARTFUN1:def 8
.= (CutLastLoc F) . f by Y, FUNCT_4:12
.= F . f by S, GRFUNC_1:8
.= F /. f by XX, PARTFUN1:def 8 ;
IC (Exec ((F /. f),s2)) in NIC ((F /. f),f) by A7;
then A12: x in dom F by A6, A11, X;
dom F c= dom (F ';' G) by COMPOS_1:103;
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, COMPOS_1:def 40;
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;
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;

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 ;
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, A16, A19, COMPOS_1:def 40
.= (IC (Exec ((G /. m),(s2 +* v)))) + k by A29, Def17
.= (IC (Exec ((G /. m),s3))) + k by A37, COMPOS_1:24 ;
IC (Exec ((G /. m),s3)) in NIC ((G /. m),m) by A32;
then IC (Exec ((G /. m),s3)) in dom G by A17;
then IC (Exec ((G /. m),s3)) in dom (IncAddr (G,k)) by COMPOS_1:def 40;
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;