let n be Nat; for p, q being FinSequence st n in dom q & p = (q /^ n) ^ (q | n) holds
q = (p /^ ((len p) -' n)) ^ (p | ((len p) -' n))
let p, q be FinSequence; ( n in dom q & p = (q /^ n) ^ (q | n) implies q = (p /^ ((len p) -' n)) ^ (p | ((len p) -' n)) )
assume that
A1:
n in dom q
and
A2:
p = (q /^ n) ^ (q | n)
; q = (p /^ ((len p) -' n)) ^ (p | ((len p) -' n))
set L = len p;
set R = ((rng p) \/ (rng q)) \/ {1};
set Ln = (len p) -' n;
( ((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 q1n = Q /^ n;
set qn = Q | n;
set pL = P | ((len p) -' n);
set p1L = P /^ ((len p) -' n);
A3:
(Q | n) ^ (Q /^ n) = q
by RFINSEQ:8;
then
(len (Q /^ n)) + (len (Q | n)) = len q
by FINSEQ_1:22;
then A4:
len p = len q
by FINSEQ_1:22, A2;
then A5:
n <= len p
by FINSEQ_3:25, A1;
then
(len p) - n = (len p) -' n
by XREAL_1:233;
then A7:
len (Q /^ n) = (len p) -' n
by A4, A5, RFINSEQ:def 1;
A8:
p = (P | ((len p) -' n)) ^ (P /^ ((len p) -' n))
by RFINSEQ:8;
P | ((len p) -' n) = q /^ n
by A2, A7, FINSEQ_5:23;
hence
q = (p /^ ((len p) -' n)) ^ (p | ((len p) -' n))
by A2, A8, FINSEQ_1:33, A3; verum