let p, q be FinSequence; :: thesis: for x being set st p = <*x*> ^ q holds
for n being non zero Nat holds p .followSet (n + 1) = q .followSet n
let x be set ; :: thesis: ( p = <*x*> ^ q implies for n being non zero Nat holds p .followSet (n + 1) = q .followSet n )
assume A1: p = <*x*> ^ q ; :: thesis: for n being non zero Nat 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:40;
then A2: len p = 1 + (len q) by A1, FINSEQ_1:22;

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:8;
then ((n + 1),(len p)) -cut p = {} by FINSEQ_6:def 4;
hence p .followSet (n + 1) = q .followSet n by A3, FINSEQ_6:def 4; :: thesis: verum

end;

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

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

A11: now :: thesis: for i being Nat st i in dom q holds
p . (i + 1) = q . i

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

end;

A12: now :: thesis: for k being Nat st k in dom ((n,(len q)) -cut q) holds
(((n + 1),(len p)) -cut p) . k = ((n,(len q)) -cut q) . k

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: k <= (len p) - n by A8, A10, A13, FINSEQ_3:25;
then A15: (- 1) + k < 0 + ((len p) - n) by XREAL_1:8;
1 <= k by A13, FINSEQ_3:25;
then 1 + (- 1) <= k + (- 1) by XREAL_1:7;
then k - 1 in NAT by INT_1:3;
then reconsider k1 = k - 1 as Nat ;
n + k <= n + ((len p) - n) by A14, XREAL_1:7;
then A16: ((k1 + n) + 1) + (- 1) <= ((len q) + 1) + (- 1) by A2, XREAL_1:7;
1 + 0 <= n + k1 by NAT_1:13;
then A17: n + k1 in dom q by A16, FINSEQ_3:25;
thus (((n + 1),(len p)) -cut p) . k = (((n + 1),(len p)) -cut p) . (k1 + 1)
.= p . ((n + 1) + k1) by A7, A5, A8, A15, FINSEQ_6:def 4
.= p . ((n + k1) + 1)
.= q . (n + k1) by A11, A17
.= ((n,(len q)) -cut q) . (k1 + 1) by A2, A4, A6, A9, A15, FINSEQ_6:def 4
.= ((n,(len q)) -cut q) . k ; :: thesis: verum

end;

now :: thesis: for y being object holds
( ( 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) ) )

let y be object ; :: 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
A18: k in dom (((n + 1),(len p)) -cut p) and
A19: (((n + 1),(len p)) -cut p) . k = y by FINSEQ_2:10;
(((n + 1),(len p)) -cut p) . k = ((n,(len q)) -cut q) . k by A10, A12, A18;
hence y in rng ((n,(len q)) -cut q) by A10, A18, A19, FUNCT_1:3; :: 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
A20: k in dom ((n,(len q)) -cut q) and
A21: ((n,(len q)) -cut q) . k = y by FINSEQ_2:10;
(((n + 1),(len p)) -cut p) . k = ((n,(len q)) -cut q) . k by A12, A20;
hence y in rng (((n + 1),(len p)) -cut p) by A10, A20, A21, FUNCT_1:3; :: thesis: verum

end;

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

end;

end;