let k, n be Nat; for p, q being FinSequence st (p /^ k) ^ (p | k) = (q /^ n) ^ (q | n) & k <= n & n <= len p holds
p = (q /^ (n -' k)) ^ (q | (n -' k))
let p, q be FinSequence; ( (p /^ k) ^ (p | k) = (q /^ n) ^ (q | n) & k <= n & n <= len p implies p = (q /^ (n -' k)) ^ (q | (n -' k)) )
assume A1:
(p /^ k) ^ (p | k) = (q /^ n) ^ (q | n)
; ( not k <= n or not n <= len p or p = (q /^ (n -' k)) ^ (q | (n -' k)) )
set nk = n -' k;
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;
assume A2:
k <= n
; ( not n <= len p or p = (q /^ (n -' k)) ^ (q | (n -' k)) )
then A3:
n - k = n -' k
by XREAL_1:233;
then A4:
(n -' k) + k = n
;
A5:
n -' k <= (n -' k) + k
by NAT_1:11;
then A6:
n -' (n -' k) = n - (n -' k)
by XREAL_1:233, A3;
(Q | n) ^ (Q /^ n) = q
by RFINSEQ:8;
then A7:
(len (Q /^ n)) + (len (Q | n)) = len q
by FINSEQ_1:22;
A8:
Q | n = ((Q | n) | (n -' k)) ^ ((Q | n) /^ (n -' k))
by RFINSEQ:8;
assume A9:
n <= len p
; p = (q /^ (n -' k)) ^ (q | (n -' k))
then reconsider Lk = (len p) - k, Ln = (len p) - n as Nat by A2, XXREAL_0:2, NAT_1:21;
A10:
len ((P /^ k) ^ (P | k)) = (len (P /^ k)) + (len (P | k))
by FINSEQ_1:22;
A11:
(P | k) ^ (P /^ k) = p
by RFINSEQ:8;
then
(len (P /^ k)) + (len (P | k)) = len p
by FINSEQ_1:22;
then
len p = len q
by A7, A10, FINSEQ_1:22, A1;
then A12:
len (Q /^ n) = Ln
by A9, RFINSEQ:def 1;
A13:
P /^ k = ((P /^ k) | Ln) ^ ((P /^ k) /^ Ln)
by RFINSEQ:8;
then A14:
(Q /^ n) ^ (Q | n) = ((P /^ k) | Ln) ^ (((P /^ k) /^ Ln) ^ (P | k))
by A1, FINSEQ_1:32;
k <= len p
by A9, A2, XXREAL_0:2;
then A15:
len (P /^ k) = Lk
by RFINSEQ:def 1;
then
len ((P /^ k) | Ln) = Ln
by A2, XREAL_1:10, FINSEQ_1:59;
then A16: (P /^ k) | Ln =
((Q /^ n) ^ (Q | n)) | Ln
by A14, FINSEQ_5:23
.=
Q /^ n
by A12, FINSEQ_5:23
;
Lk >= Ln
by A2, XREAL_1:10;
then A17:
len ((P /^ k) /^ Ln) = Lk - Ln
by A15, RFINSEQ:def 1;
A18: (Q | n) | (n -' k) =
(((P /^ k) /^ Ln) ^ (P | k)) | (n -' k)
by A16, A14, FINSEQ_1:33
.=
(P /^ k) /^ Ln
by A17, FINSEQ_5:23, A3
;
Q | n = ((P /^ k) /^ Ln) ^ (P | k)
by A16, A14, FINSEQ_1:33;
then
(Q | n) /^ (n -' k) = P | k
by A18, A8, FINSEQ_1:33;
hence p =
((Q /^ (n -' k)) | k) ^ ((Q /^ n) ^ ((Q | n) | (n -' k)))
by A6, FINSEQ_5:80, A3, A13, A16, A18, A11
.=
((Q /^ (n -' k)) | k) ^ (((Q /^ (n -' k)) /^ k) ^ ((Q | n) | (n -' k)))
by FINSEQ_6:81, A4
.=
(((Q /^ (n -' k)) | k) ^ ((Q /^ (n -' k)) /^ k)) ^ ((Q | n) | (n -' k))
by FINSEQ_1:32
.=
(Q /^ (n -' k)) ^ ((Q | n) | (n -' k))
by RFINSEQ:8
.=
(q /^ (n -' k)) ^ (q | (n -' k))
by A5, FINSEQ_1:82, A3
;
verum