set f = id NAT;
for i, k being Nat st i in dom (id NAT) & k in dom (id NAT) holds
((id NAT) . (k + 1)) - ((id NAT) . k) = ((id NAT) . (i + 1)) - ((id NAT) . i)

proof

let i, k be Nat; :: thesis: ( i in dom (id NAT) & k in dom (id NAT) implies ((id NAT) . (k + 1)) - ((id NAT) . k) = ((id NAT) . (i + 1)) - ((id NAT) . i) )
assume ( i in dom (id NAT) & k in dom (id NAT) ) ; :: thesis: ((id NAT) . (k + 1)) - ((id NAT) . k) = ((id NAT) . (i + 1)) - ((id NAT) . i)
A7: ((id NAT) . (i + 1)) - ((id NAT) . i) = (i + 1) - i by ORDINAL1:def 12, FUNCT_1:18;
((id NAT) . (k + 1)) - ((id NAT) . k) = (k + 1) - k by ORDINAL1:def 12, FUNCT_1:18
.= 1 ;
hence ((id NAT) . (k + 1)) - ((id NAT) . k) = ((id NAT) . (i + 1)) - ((id NAT) . i) by A7; :: thesis: verum

end;

hence id NAT is AP-like ; :: thesis: verum