let w be FinSequence of INT ; :: thesis: for f being FinSeq-Location
for s being State of SCM+FSA
for I being Program of {INT,(INT *)} holds ProgramPart ((Initialized I) +* (f .--> w)) = I
let f be FinSeq-Location ; :: thesis: for s being State of SCM+FSA
for I being Program of {INT,(INT *)} holds ProgramPart ((Initialized I) +* (f .--> w)) = I
let s be State of SCM+FSA; :: thesis: for I being Program of {INT,(INT *)} holds ProgramPart ((Initialized I) +* (f .--> w)) = I
let I be Program of {INT,(INT *)}; :: thesis: ProgramPart ((Initialized I) +* (f .--> w)) = I
not f in NAT by SCMFSA10:4;
then (f .--> w) | NAT = {} by FUNCOP_1:91;
then f .--> w is program-free by COMPOS_1:def 29;
hence ProgramPart ((Initialized I) +* (f .--> w)) = ProgramPart (Initialized I) by COMPOS_1:66
.= I by SCMFSA6A:33 ;
:: thesis: verum