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

proof

let i, k be Nat; :: thesis: ( i in dom (f | n) & k in dom (f | n) & i + 1 in dom (f | n) & k + 1 in dom (f | n) implies ((f | n) . (i + 1)) - ((f | n) . i) = ((f | n) . (k + 1)) - ((f | n) . k) )
A0: dom (f | n) c= dom f by RELAT_1:60;
assume a1: ( i in dom (f | n) & k in dom (f | n) & i + 1 in dom (f | n) & k + 1 in dom (f | n) ) ; :: thesis: ((f | n) . (i + 1)) - ((f | n) . i) = ((f | n) . (k + 1)) - ((f | n) . k)
then A2: ( f . (i + 1) = (f | n) . (i + 1) & (f | n) . (k + 1) = f . (k + 1) ) by FUNCT_1:47;
( f . i = (f | n) . i & (f | n) . k = f . k ) by a1, FUNCT_1:47;
hence ((f | n) . (i + 1)) - ((f | n) . i) = ((f | n) . (k + 1)) - ((f | n) . k) by A2, a1, A0, APLikeDef; :: thesis: verum

end;

hence f | n is AP-like ; :: thesis: verum