set P = F ';' G;
set k = (card F) -' 1;
let f be Nat; :: according to AMISTD_1:def 9 :: thesis: ( not f in K497(omega,(F ';' G)) or NIC (((F ';' G) /. f),f) c= K497(omega,(F ';' G)) )
assume A1: f in dom (F ';' G) ; :: thesis: NIC (((F ';' G) /. f),f) c= K497(omega,(F ';' G))
A2: dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Reloc (G,((card F) -' 1)))) by FUNCT_4:def 1;
A3: dom (CutLastLoc F) c= dom F by GRFUNC_1:2;
A4: dom (Reloc (G,((card F) -' 1))) = { (m + ((card F) -' 1)) where m is Nat : m in dom (IncAddr (G,((card F) -' 1))) } by VALUED_1:def 12;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NIC (((F ';' G) /. f),f) or x in K497(omega,(F ';' G)) )
assume x in NIC (((F ';' G) /. f),f) ; :: thesis: x in K497(omega,(F ';' G))
then consider s2 being Element of product (the_Values_of S) such that
A5: x = IC (Exec (((F ';' G) /. f),s2)) and
A6: IC s2 = f ;
A7: (F ';' G) /. f = (F ';' G) . f by A1, PARTFUN1:def 6;

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

suppose A8: f in dom (CutLastLoc F) ; :: thesis: x in K497(omega,(F ';' G))

then A9: NIC ((F /. f),f) c= dom F by A3, AMISTD_1:def 9;
dom (CutLastLoc F) = (dom F) \ {(LastLoc F)} by VALUED_1:36;
then A10: f in dom F by A8;
dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1))) by COMPOS_1:18;
then A11: not f in dom (Reloc (G,((card F) -' 1))) by A8, XBOOLE_0:3;
A12: (F ';' G) /. f = (F ';' G) . f by A1, PARTFUN1:def 6
.= (CutLastLoc F) . f by A11, FUNCT_4:11
.= F . f by A8, GRFUNC_1:2
.= F /. f by A10, PARTFUN1:def 6 ;
IC (Exec ((F /. f),s2)) in NIC ((F /. f),f) by A6;
then A13: x in dom F by A5, A9, A12;
dom F c= dom (F ';' G) by COMPOS_1:21;
hence x in K497(omega,(F ';' G)) by A13; :: thesis: verum

end;

suppose A14: f in dom (Reloc (G,((card F) -' 1))) ; :: thesis: x in K497(omega,(F ';' G))

then consider m being Nat such that
A15: f = m + ((card F) -' 1) and
A16: m in dom (IncAddr (G,((card F) -' 1))) by A4;
A17: m in dom G by A16, COMPOS_1:def 21;
then A18: NIC ((G /. m),m) c= dom G by AMISTD_1:def 9;
A19: Values (IC ) = NAT by MEMSTR_0:def 6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
reconsider v = (IC ) .--> m as FinPartState of S by A19;
set s1 = s2 +* v;
A20: (F ';' G) /. f = (Reloc (G,((card F) -' 1))) . f by A7, A14, FUNCT_4:13
.= (IncAddr (G,((card F) -' 1))) . m by A15, A16, VALUED_1:def 12 ;
A21: ((IC ) .--> m) . (IC ) = m by FUNCOP_1:72;
A22: IC in {(IC )} by TARSKI:def 1;
A23: dom ((IC ) .--> m) = {(IC )} ;
reconsider w = (IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1)) as FinPartState of S by A19;
A24: dom ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) = the carrier of S by PARTFUN1:def 2;
A25: dom s2 = the carrier of S by PARTFUN1:def 2;
for a being object st a in dom s2 holds
s2 . a = ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) . a

proof

let a be object ; :: thesis: ( a in dom s2 implies s2 . a = ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) . a )
assume a in dom s2 ; :: thesis: s2 . a = ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) . a
A26: dom ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1))) = {(IC )} ;

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

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

hence s2 . a = (IC (s2 +* v)) + ((card F) -' 1) by A6, A15, A23, A21, A22, FUNCT_4:13
.= ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1))) . a by A27, FUNCOP_1:72
.= ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) . a by A22, A26, A27, FUNCT_4:13 ;
:: thesis: verum

end;

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

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

end;

end;

end;

then A30: s2 = IncIC ((s2 +* v),((card F) -' 1)) by A24, A25, FUNCT_1:2;
set s3 = s2 +* v;
A31: IC (s2 +* v) = m by A21, A22, A23, FUNCT_4:13;
reconsider s3 = s2 +* v as Element of product (the_Values_of S) by CARD_3:107;
reconsider k = (card F) -' 1, m = m as Element of NAT ;
A32: x = IC (Exec ((IncAddr ((G /. m),k)),s2)) by A5, A17, A20, COMPOS_1:def 21
.= (IC (Exec ((G /. m),s3))) + k by A30, Th7 ;
IC (Exec ((G /. m),s3)) in NIC ((G /. m),m) by A31;
then IC (Exec ((G /. m),s3)) in dom G by A18;
then IC (Exec ((G /. m),s3)) in dom (IncAddr (G,k)) by COMPOS_1:def 21;
then x in dom (Reloc (G,k)) by A4, A32;
hence x in K497(omega,(F ';' G)) by A2, XBOOLE_0:def 3; :: thesis: verum

end;

end;