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 A2, FINSEQ_3:25;

hereby :: thesis: ( x .. p >= n implies x in p .followSet n )

A5: p . (x .. p) = x by A1, FINSEQ_4:19;
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 A1, FINSEQ_4:20;
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 A6, GRAPH_3:2;
hence x .. p >= n by A3, A7, A8, A5, FUNCT_1:def 4; :: 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 A2, FINSEQ_3:25;
then A11: (len ((n,(len p)) -cut p)) + n = (len p) + 1 by A4, FINSEQ_6:def 4;
x .. p in dom p by A1, FINSEQ_4:20;
then k + n <= len p by A9, FINSEQ_3:25;
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 A11, NAT_1:13;
then A13: ((n,(len p)) -cut p) . (k + 1) = p . (x .. p) by A9, A10, A4, FINSEQ_6:def 4;
A14: p . (x .. p) = x by A1, FINSEQ_4:19;
0 + 1 <= k + 1 by XREAL_1:7;
then k + 1 in dom ((n,(len p)) -cut p) by A11, A12, FINSEQ_3:25;
hence x in p .followSet n by A14, A13, FUNCT_1:3; :: thesis: verum