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

proof

let i, k be Nat; :: thesis: ( i in dom (id REAL) & k in dom (id REAL) implies ((id REAL) . (k + 1)) - ((id REAL) . k) = ((id REAL) . (i + 1)) - ((id REAL) . i) )
assume ( i in dom (id REAL) & k in dom (id REAL) ) ; :: thesis: ((id REAL) . (k + 1)) - ((id REAL) . k) = ((id REAL) . (i + 1)) - ((id REAL) . i)
A8: ( (id REAL) . (i + 1) = i + 1 & (id REAL) . i = i ) by XREAL_0:def 1, FUNCT_1:18;
( (id REAL) . (k + 1) = k + 1 & (id REAL) . k = k ) by XREAL_0:def 1, FUNCT_1:18;
then ((id REAL) . (k + 1)) - ((id REAL) . k) = 1 ;
hence ((id REAL) . (k + 1)) - ((id REAL) . k) = ((id REAL) . (i + 1)) - ((id REAL) . i) by A8; :: thesis: verum

end;

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