let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N
for F being NAT -defined FinPartState of holds IncAddr F,0 = F
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N; :: thesis: for F being NAT -defined FinPartState of holds IncAddr F,0 = F
let F be NAT -defined FinPartState of ; :: thesis: IncAddr F,0 = F
for m being natural number st il. S,m in dom F holds
F . (il. S,m) = IncAddr (pi F,(il. S,m)),0

proof

let m be natural number ; :: thesis: ( il. S,m in dom F implies F . (il. S,m) = IncAddr (pi F,(il. S,m)),0 )
assume il. S,m in dom F ; :: thesis: F . (il. S,m) = IncAddr (pi F,(il. S,m)),0
then pi F,(il. S,m) = F . (il. S,m) by AMI_1:def 47;
hence F . (il. S,m) = IncAddr (pi F,(il. S,m)),0 by Th28; :: thesis: verum

end;

hence IncAddr F,0 = F by Def15; :: thesis: verum