let p be FinSequence; :: thesis: for x being set
for n being Nat st x in rng p & n in dom p & p is one-to-one holds
( x in p .followSet n iff x .. p >= n )

let x be set ; :: thesis: for n being Nat st x in rng p & n in dom p & p is one-to-one holds
( x in p .followSet n iff x .. p >= n )

let n be Nat; :: thesis: ( x in rng p & n in dom p & p is one-to-one implies ( x in p .followSet n iff x .. p >= n ) )
assume that
A1: x in rng p and
A2: n in dom p and
A3: p is one-to-one ; :: thesis: ( x in p .followSet n iff x .. p >= n )
A4: n <= len p by ;
hereby :: thesis: ( x .. p >= n implies x in p .followSet n )
A5: p . (x .. p) = x by ;
assume x in p .followSet n ; :: thesis: x .. p >= n
then consider a being Nat such that
A6: a in dom ((n,(len p)) -cut p) and
A7: ((n,(len p)) -cut p) . a = x by FINSEQ_2:10;
A8: x .. p in dom p by ;
ex k being Nat st
( k in dom p & p . k = ((n,(len p)) -cut p) . a & k + 1 = n + a & n <= k & k <= len p ) by ;
hence x .. p >= n by ; :: thesis: verum
end;
assume x .. p >= n ; :: thesis: x in p .followSet n
then consider k being Nat such that
A9: x .. p = n + k by NAT_1:10;
A10: 1 <= n by ;
then A11: (len ((n,(len p)) -cut p)) + n = (len p) + 1 by ;
x .. p in dom p by ;
then k + n <= len p by ;
then (k + n) + (- n) <= (len p) + (- n) by XREAL_1:7;
then A12: k + 1 <= ((len p) - n) + 1 by XREAL_1:7;
then k < len ((n,(len p)) -cut p) by ;
then A13: ((n,(len p)) -cut p) . (k + 1) = p . (x .. p) by ;
A14: p . (x .. p) = x by ;
0 + 1 <= k + 1 by XREAL_1:7;
then k + 1 in dom ((n,(len p)) -cut p) by ;
hence x in p .followSet n by ; :: thesis: verum