let n be Nat; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum