reconsider ii = id NAT as sequence of REAL by FUNCT_2:7, NUMBERS:19;
set n = the Nat;
set f = ii | the Nat;
A1: ii | the Nat is XFinSequence by RestrictedXFin;
for i, k being Nat st i in dom (ii | the Nat) & i + 1 in dom (ii | the Nat) & k in dom (ii | the Nat) & k + 1 in dom (ii | the Nat) holds
((ii | the Nat) . (k + 1)) - ((ii | the Nat) . k) = ((ii | the Nat) . (i + 1)) - ((ii | the Nat) . i)

proof

let i, k be Nat; :: thesis: ( i in dom (ii | the Nat) & i + 1 in dom (ii | the Nat) & k in dom (ii | the Nat) & k + 1 in dom (ii | the Nat) implies ((ii | the Nat) . (k + 1)) - ((ii | the Nat) . k) = ((ii | the Nat) . (i + 1)) - ((ii | the Nat) . i) )
assume B1: ( i in dom (ii | the Nat) & i + 1 in dom (ii | the Nat) & k in dom (ii | the Nat) & k + 1 in dom (ii | the Nat) ) ; :: thesis: ((ii | the Nat) . (k + 1)) - ((ii | the Nat) . k) = ((ii | the Nat) . (i + 1)) - ((ii | the Nat) . i)
then B2: (ii | the Nat) . (k + 1) = ii . (k + 1) by FUNCT_1:47
.= k + 1 ;
B3: (ii | the Nat) . (i + 1) = ii . (i + 1) by B1, FUNCT_1:47
.= i + 1 ;
B4: (ii | the Nat) . i = ii . i by B1, FUNCT_1:47
.= i by FUNCT_1:18, ORDINAL1:def 12 ;
(ii | the Nat) . k = ii . k by B1, FUNCT_1:47
.= k by FUNCT_1:18, ORDINAL1:def 12 ;
then ((ii | the Nat) . (k + 1)) - ((ii | the Nat) . k) = ((ii | the Nat) . (i + 1)) - ((ii | the Nat) . i) by B2, B3, B4;
hence ((ii | the Nat) . (k + 1)) - ((ii | the Nat) . k) = ((ii | the Nat) . (i + 1)) - ((ii | the Nat) . i) ; :: thesis: verum

end;

then ii | the Nat is AP-like ;
hence ex b₁ being real-valued integer-valued XFinSequence st b₁ is AP-like by A1; :: thesis: verum