let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA holds DataPart (Initialized s) = DataPart (s +* (Initialized I))
let I be Program of SCM+FSA ; :: thesis: DataPart (Initialized s) = DataPart (s +* (Initialized I))
set s1 = s +* (Initialized I);

A1: now

let a be Int-Location ; :: thesis: (s +* (Initialized I)) . b₁ = (Initialized s) . b₁

per cases ( intloc 0 = a or intloc 0 <> a ) ;

suppose A2: intloc 0 = a ; :: thesis: (s +* (Initialized I)) . b₁ = (Initialized s) . b₁

then a in dom (Initialized I) by SCMFSA6A:45;
hence (s +* (Initialized I)) . a = (Initialized I) . (intloc 0 ) by A2, FUNCT_4:14
.= 1 by SCMFSA6A:46
.= (Initialized s) . a by A2, SCMFSA6C:3 ;
:: thesis: verum

end;

suppose A3: intloc 0 <> a ; :: thesis: (s +* (Initialized I)) . b₁ = (Initialized s) . b₁

then A4: not a is read-only by SF_MASTR:def 5;
not a in dom (Initialized I) by A3, SCMFSA6A:48;
hence (s +* (Initialized I)) . a = s . a by FUNCT_4:12
.= (Initialized s) . a by A4, SCMFSA6C:3 ;
:: thesis: verum

end;

end;

end;

now

let f be FinSeq-Location ; :: thesis: (s +* (Initialized I)) . f = (Initialized s) . f
not f in dom (Initialized I) by SCMFSA6A:49;
hence (s +* (Initialized I)) . f = s . f by FUNCT_4:12
.= (Initialized s) . f by SCMFSA6C:3 ;
:: thesis: verum

end;

hence DataPart (Initialized s) = DataPart (s +* (Initialized I)) by A1, SCMFSA6A:38; :: thesis: verum