for m being Nat st m in dom F holds
F . m = IncAddr ((F /. m),0)
proof
let m be Nat; :: 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 COMPOS_0:3; :: thesis: verum
end;
hence IncAddr (F,0) = F by Def9; :: thesis: verum