let f be real-valued FinSequence; :: thesis: ( f is constant implies f is fAP-like )
assume A1: f is constant ; :: thesis: f is fAP-like
for i being Nat st i in dom f & i + 1 in dom f & i + 2 in dom f holds
(f . (i + 2)) - (f . (i + 1)) = (f . (i + 1)) - (f . i)

proof

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

end;

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