let S be standard-ins homogeneous regular J/A-independent COM-Struct ; :: thesis: for F being NAT -defined the Instructions of S -valued finite Function holds IncAddr (F,0) = F
let F be NAT -defined the Instructions of S -valued finite Function; :: thesis: IncAddr (F,0) = F
for m being natural number st m in dom F holds
F . m = IncAddr ((F /. m),0)

proof

let m be natural number ; :: thesis: ( m in dom F implies F . m = IncAddr ((F /. m),0) )
assume m in dom F ; :: thesis: F . m = IncAddr ((F /. m),0)
then F /. m = F . m by PARTFUN1:def 6;
hence F . m = IncAddr ((F /. m),0) by Th91; :: thesis: verum

end;

hence IncAddr (F,0) = F by Def40; :: thesis: verum