let p be FinSequence; :: thesis: for x being set
for n being natural number 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 natural number 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 )
hereby :: thesis: ( x .. p >= n implies x in p .followSet n )
assume
x in p .followSet n
;
:: thesis: x .. p >= nthen consider a being
Nat such that A4:
a in dom (n,(len p) -cut p)
and A5:
(n,(len p) -cut p) . a = x
by FINSEQ_2:11;
n in NAT
by ORDINAL1:def 13;
then consider k being
Element of
NAT such that A6:
k in dom p
and A7:
p . k = (n,(len p) -cut p) . a
and
k + 1
= n + a
and A8:
(
n <= k &
k <= len p )
by A4, GRAPH_3:2;
A9:
x .. p in dom p
by A1, FINSEQ_4:30;
p . (x .. p) = x
by A1, FINSEQ_4:29;
hence
x .. p >= n
by A3, A5, A6, A7, A8, A9, FUNCT_1:def 8;
:: thesis: verum
end;
assume A10:
x .. p >= n
; :: thesis: x in p .followSet n
A11:
p . (x .. p) = x
by A1, FINSEQ_4:29;
consider k being Nat such that
A12:
x .. p = n + k
by A10, NAT_1:10;
A13:
( 1 <= n & n <= len p )
by A2, FINSEQ_3:27;
then A14:
(len (n,(len p) -cut p)) + n = (len p) + 1
by GRAPH_2:def 1;
x .. p in dom p
by A1, FINSEQ_4:30;
then
k + n <= len p
by A12, FINSEQ_3:27;
then
(k + n) + (- n) <= (len p) + (- n)
by XREAL_1:9;
then A15:
k + 1 <= ((len p) - n) + 1
by XREAL_1:9;
0 + 1 <= k + 1
by XREAL_1:9;
then A16:
k + 1 in dom (n,(len p) -cut p)
by A14, A15, FINSEQ_3:27;
k < len (n,(len p) -cut p)
by A14, A15, NAT_1:13;
then
(n,(len p) -cut p) . (k + 1) = p . (x .. p)
by A12, A13, GRAPH_2:def 1;
hence
x in p .followSet n
by A11, A16, FUNCT_1:12; :: thesis: verum