let k, n be Nat; :: thesis: for p, q being FinSequence st (p /^ k) ^ (p | k) = (q /^ n) ^ (q | n) holds
ex i being Nat st p = (q /^ i) ^ (q | i)
let p, q be FinSequence; :: thesis: ( (p /^ k) ^ (p | k) = (q /^ n) ^ (q | n) implies ex i being Nat st p = (q /^ i) ^ (q | i) )
assume A1: (p /^ k) ^ (p | k) = (q /^ n) ^ (q | n) ; :: thesis: ex i being Nat st p = (q /^ i) ^ (q | i)
set L = len p;
set R = ((rng p) \/ (rng q)) \/ {1};
( ((rng p) \/ (rng q)) \/ {1} = (rng p) \/ ((rng q) \/ {1}) & ((rng p) \/ (rng q)) \/ {1} = (rng q) \/ ((rng p) \/ {1}) ) by XBOOLE_1:4;
then reconsider P = p, Q = q as FinSequence of ((rng p) \/ (rng q)) \/ {1} by XBOOLE_1:7, FINSEQ_1:def 4;
set p1k = P /^ k;
set pk = P | k;
set q1n = Q /^ n;
set qn = Q | n;
(P | k) ^ (P /^ k) = p by RFINSEQ:8;
then A2: (len (P /^ k)) + (len (P | k)) = len p by FINSEQ_1:22;
(Q | n) ^ (Q /^ n) = q by RFINSEQ:8;
then A3: (len (Q /^ n)) + (len (Q | n)) = len q by FINSEQ_1:22;
len ((P /^ k) ^ (P | k)) = (len (P /^ k)) + (len (P | k)) by FINSEQ_1:22;
then A4: len p = len q by A2, A3, FINSEQ_1:22, A1;

per cases ( not k in dom p or ( not n in dom q & k in dom p ) or ( n in dom q & k in dom p & k <= n ) or ( n in dom q & k in dom p & k > n ) ) ;

suppose not k in dom p ; :: thesis: ex i being Nat st p = (q /^ i) ^ (q | i)

then p = (q /^ n) ^ (q | n) by A1, Lm4;
hence ex i being Nat st p = (q /^ i) ^ (q | i) ; :: thesis: verum

end;

suppose A5: ( not n in dom q & k in dom p ) ; :: thesis: ex i being Nat st p = (q /^ i) ^ (q | i)

then q = (p /^ k) ^ (p | k) by Lm4, A1;
then p = (q /^ ((len q) -' k)) ^ (q | ((len q) -' k)) by A5, Th4;
hence ex i being Nat st p = (q /^ i) ^ (q | i) ; :: thesis: verum

end;

suppose A6: ( n in dom q & k in dom p & k <= n ) ; :: thesis: ex i being Nat st p = (q /^ i) ^ (q | i)

then n <= len p by A4, FINSEQ_3:25;
then p = (q /^ (n -' k)) ^ (q | (n -' k)) by A6, A1, Th3;
hence ex i being Nat st p = (q /^ i) ^ (q | i) ; :: thesis: verum

end;

suppose A7: ( n in dom q & k in dom p & k > n ) ; :: thesis: ex i being Nat st p = (q /^ i) ^ (q | i)

then A8: k -' n = k - n by XREAL_1:233;
then k -' n <> 0 by A7;
then A9: k -' n >= 1 by NAT_1:14;
A10: k <= len p by A7, FINSEQ_3:25;
k -' n <= (k -' n) + n by NAT_1:11;
then k -' n <= len p by A8, XXREAL_0:2, A10;
then A11: k -' n in dom p by A9, FINSEQ_3:25;
q = (p /^ (k -' n)) ^ (p | (k -' n)) by A10, A4, A7, A1, Th3;
then p = (q /^ ((len q) -' (k -' n))) ^ (q | ((len q) -' (k -' n))) by A11, Th4;
hence ex i being Nat st p = (q /^ i) ^ (q | i) ; :: thesis: verum

end;

end;