let p, q be FinSequence; :: thesis: for x being set st p = <*x*> ^ q holds
for n being non zero natural number holds p .followSet (n + 1) = q .followSet n
let x be set ; :: thesis: ( p = <*x*> ^ q implies for n being non zero natural number holds p .followSet (n + 1) = q .followSet n )
assume A1: p = <*x*> ^ q ; :: thesis: for n being non zero natural number holds p .followSet (n + 1) = q .followSet n
let n be non zero Nat; :: thesis: p .followSet (n + 1) = q .followSet n
len <*x*> = 1 by FINSEQ_1:57;
then A2: len p = 1 + (len q) by A1, FINSEQ_1:35;

per cases ( n > len q or n <= len q ) ;

suppose A3: n > len q ; :: thesis: p .followSet (n + 1) = q .followSet n

then n + 1 > len p by A2, XREAL_1:10;
then (n + 1),(len p) -cut p = {} by GRAPH_2:def 1;
hence p .followSet (n + 1) = q .followSet n by A3, GRAPH_2:def 1; :: thesis: verum

end;

suppose A4: n <= len q ; :: thesis: p .followSet (n + 1) = q .followSet n

A5: 0 + 1 <= n by NAT_1:13;
then A6: (len (n,(len q) -cut q)) + n = (len q) + 1 by A4, GRAPH_2:def 1;
A7: ( 1 <= n + 1 & n + 1 <= len p & len p <= len p ) by A2, A4, A5, XREAL_1:9;
then A8: (len ((n + 1),(len p) -cut p)) + (n + 1) = (len p) + 1 by GRAPH_2:def 1;
then dom ((n + 1),(len p) -cut p) = Seg (len (n,(len q) -cut q)) by A2, A6, FINSEQ_1:def 3;
then A9: dom ((n + 1),(len p) -cut p) = dom (n,(len q) -cut q) by FINSEQ_1:def 3;

A10: now

let i be Nat; :: thesis: ( i in dom q implies p . (i + 1) = q . i )
assume A11: i in dom q ; :: thesis: p . (i + 1) = q . i
p . ((len <*x*>) + i) = q . i by A1, A11, FINSEQ_1:def 7;
hence p . (i + 1) = q . i by FINSEQ_1:57; :: thesis: verum

end;

A12: now

let k be Nat; :: thesis: ( k in dom (n,(len q) -cut q) implies ((n + 1),(len p) -cut p) . k = (n,(len q) -cut q) . k )
assume A13: k in dom (n,(len q) -cut q) ; :: thesis: ((n + 1),(len p) -cut p) . k = (n,(len q) -cut q) . k
A14: ( 1 <= k & k <= (len p) - n ) by A8, A9, A13, FINSEQ_3:27;
then A15: n + k <= n + ((len p) - n) by XREAL_1:9;
1 + (- 1) <= k + (- 1) by A14, XREAL_1:9;
then k - 1 in NAT by INT_1:16;
then reconsider k1 = k - 1 as Nat ;
A16: (- 1) + k < 0 + ((len p) - n) by A14, XREAL_1:10;
A17: ((k1 + n) + 1) + (- 1) <= ((len q) + 1) + (- 1) by A2, A15, XREAL_1:9;
1 + 0 <= n + k1 by NAT_1:13;
then A18: n + k1 in dom q by A17, FINSEQ_3:27;
thus ((n + 1),(len p) -cut p) . k = ((n + 1),(len p) -cut p) . (k1 + 1)
.= p . ((n + 1) + k1) by A7, A8, A16, GRAPH_2:def 1
.= p . ((n + k1) + 1)
.= q . (n + k1) by A10, A18
.= (n,(len q) -cut q) . (k1 + 1) by A2, A4, A5, A6, A16, GRAPH_2:def 1
.= (n,(len q) -cut q) . k ; :: thesis: verum

end;

now

let y be set ; :: thesis: ( ( y in rng ((n + 1),(len p) -cut p) implies y in rng (n,(len q) -cut q) ) & ( y in rng (n,(len q) -cut q) implies y in rng ((n + 1),(len p) -cut p) ) )

hereby :: thesis: ( y in rng (n,(len q) -cut q) implies y in rng ((n + 1),(len p) -cut p) )

assume y in rng ((n + 1),(len p) -cut p) ; :: thesis: y in rng (n,(len q) -cut q)
then consider k being Nat such that
A19: k in dom ((n + 1),(len p) -cut p) and
A20: ((n + 1),(len p) -cut p) . k = y by FINSEQ_2:11;
((n + 1),(len p) -cut p) . k = (n,(len q) -cut q) . k by A9, A12, A19;
hence y in rng (n,(len q) -cut q) by A9, A19, A20, FUNCT_1:12; :: thesis: verum

end;

assume y in rng (n,(len q) -cut q) ; :: thesis: y in rng ((n + 1),(len p) -cut p)
then consider k being Nat such that
A21: k in dom (n,(len q) -cut q) and
A22: (n,(len q) -cut q) . k = y by FINSEQ_2:11;
((n + 1),(len p) -cut p) . k = (n,(len q) -cut q) . k by A12, A21;
hence y in rng ((n + 1),(len p) -cut p) by A9, A21, A22, FUNCT_1:12; :: thesis: verum

end;

hence p .followSet (n + 1) = q .followSet n by TARSKI:2; :: thesis: verum

end;

end;