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 ;
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 ;
then ((n + 1),(len p)) -cut p = {} by FINSEQ_6:def 4;
hence p .followSet (n + 1) = q .followSet n by ; :: thesis: verum
end;
suppose A4: n <= len q ; :: thesis: p .followSet (n + 1) = q .followSet n
then A5: n + 1 <= len p by ;
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 ;
A9: (len ((n,(len q)) -cut q)) + n = (len q) + 1 by ;
then dom (((n + 1),(len p)) -cut p) = Seg (len ((n,(len q)) -cut q)) by ;
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 . (() + i) = q . i by ;
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 ;
then A15: (- 1) + k < 0 + ((len p) - n) by XREAL_1:8;
1 <= k by ;
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 ;
then A16: ((k1 + n) + 1) + (- 1) <= ((len q) + 1) + (- 1) by ;
1 + 0 <= n + k1 by NAT_1:13;
then A17: n + k1 in dom q by ;
thus (((n + 1),(len p)) -cut p) . k = (((n + 1),(len p)) -cut p) . (k1 + 1)
.= p . ((n + 1) + k1) by
.= p . ((n + k1) + 1)
.= q . (n + k1) by
.= ((n,(len q)) -cut q) . (k1 + 1) by
.= ((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 ;
hence y in rng ((n,(len q)) -cut q) by ; :: 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 ;
hence y in rng (((n + 1),(len p)) -cut p) by ; :: thesis: verum
end;
hence p .followSet (n + 1) = q .followSet n by TARSKI:2; :: thesis: verum
end;
end;