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;

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

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 )

assume
x .. p >= n
; :: thesis: x in p .followSet nA5:
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 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

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