let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated Mem-Struct of 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 IC-Ins-separated Mem-Struct of 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

Data-Locations = (dom s2) /\ (Data-Locations ) by Th49, XBOOLE_1:28;
then A6: dom (DataPart s2) = Data-Locations by RELAT_1:61;
let x be set ; :: 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 A9: x in {(IC )} ; :: thesis: p . b₁ = s . b₁

x = IC by A9, 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 A11: x in Data-Locations ; :: thesis: p . b₁ = s . b₁

set DPp = DataPart p;
x in (dom p) /\ (Data-Locations ) by A11, A7, XBOOLE_0:def 4;
then A12: x in dom (DataPart p) by RELAT_1:61;
YY: DataPart (IncIC (p,k)) = DataPart p by Th48;
DataPart p c= IncIC (p,k) by YY, RELAT_1:59;
then A13: 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 A11, A12, XBOOLE_0:def 4;
then A14: x in dom (DataPart s2) by RELAT_1:61;
DataPart p c= p by RELAT_1:59;
then A15: (DataPart p) . x = p . x by A12, GRFUNC_1:2;
A16: s2 . x = (DataPart s2) . x by A11, FUNCT_1:49;
(DataPart p) . x = s2 . x by A12, A13, GRFUNC_1:2;
hence p . x = s . x by A15, A16, A14, 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