let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for k being Nat
for p being PartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; :: thesis: for k being Nat
for p being PartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
let k be Nat; :: thesis: for p being PartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
let p be PartState of S; :: thesis: for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
let s1, s2 be State of S; :: thesis: ( p c= s1 & IncIC (p,k) c= s2 implies p c= s1 +* (DataPart s2) )
assume that
A1: p c= s1 and
A2: IncIC (p,k) c= s2 ; :: thesis: p c= s1 +* (DataPart s2)
set s3 = DataPart s2;
reconsider s = s1 +* (DataPart s2) as State of S ;
A3: dom p c= the carrier of S by RELAT_1:def 18;
then A4: dom p c= {(IC )} \/ (Data-Locations ) by STRUCT_0:4;

A5: now :: thesis: for x being object st x in dom p holds
p . x = s . x

Data-Locations = (dom s2) /\ (Data-Locations ) by Th8, XBOOLE_1:28;
then A6: dom (DataPart s2) = Data-Locations by RELAT_1:61;
let x be object ; :: thesis: ( x in dom p implies p . b₁ = s . b₁ )
assume A7: x in dom p ; :: thesis: p . b₁ = s . b₁

per cases ( x in {(IC )} or x in Data-Locations ) by A4, A7, XBOOLE_0:def 3;

suppose A8: x in {(IC )} ; :: thesis: p . b₁ = s . b₁

x = IC by A8, TARSKI:def 1;
then s1 . x = s . x by A6, FUNCT_4:11, STRUCT_0:3;
hence p . x = s . x by A1, A7, GRFUNC_1:2; :: thesis: verum

end;

suppose A9: x in Data-Locations ; :: thesis: p . b₁ = s . b₁

set DPp = DataPart p;
x in (dom p) /\ (Data-Locations ) by A9, A7, XBOOLE_0:def 4;
then A10: x in dom (DataPart p) by RELAT_1:61;
A11: DataPart (IncIC (p,k)) = DataPart p by Th51;
DataPart p c= IncIC (p,k) by A11, RELAT_1:59;
then A12: DataPart p c= s2 by A2, XBOOLE_1:1;
then dom (DataPart p) c= dom s2 by GRFUNC_1:2;
then x in (dom s2) /\ (Data-Locations ) by A9, A10, XBOOLE_0:def 4;
then A13: x in dom (DataPart s2) by RELAT_1:61;
DataPart p c= p by RELAT_1:59;
then A14: (DataPart p) . x = p . x by A10, GRFUNC_1:2;
A15: s2 . x = (DataPart s2) . x by A9, FUNCT_1:49;
(DataPart p) . x = s2 . x by A10, A12, GRFUNC_1:2;
hence p . x = s . x by A14, A15, A13, FUNCT_4:13; :: thesis: verum

end;

end;

end;

dom p c= dom s by A3, PARTFUN1:def 2;
hence p c= s1 +* (DataPart s2) by A5, GRFUNC_1:2; :: thesis: verum