let f be sequence of REAL; :: thesis: ( f is constant implies f is AP-like )
assume A1: f is constant ; :: thesis: f is AP-like
AA: dom f = NAT by FUNCT_2:def 1;
for i, k being Nat st i in dom f & k in dom f holds
(f . (i + 1)) - (f . i) = (f . (k + 1)) - (f . k)

proof

let i, k be Nat; :: thesis: ( i in dom f & k in dom f implies (f . (i + 1)) - (f . i) = (f . (k + 1)) - (f . k) )
assume A4: ( i in dom f & k in dom f ) ; :: thesis: (f . (i + 1)) - (f . i) = (f . (k + 1)) - (f . k)
then A7: f . (i + 1) = f . i by A1, AA, FUNCT_1:def 10;
f . (k + 1) = f . k by A1, AA, A4, FUNCT_1:def 10;
hence (f . (i + 1)) - (f . i) = (f . (k + 1)) - (f . k) by A7; :: thesis: verum

end;

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