set n = len p;
let q1, q2 be Element of S ^^ (len p); ( decomp (S,(len p),q1) = p & decomp (S,(len p),q2) = p implies q1 = q2 )
assume that
A1:
decomp (S,(len p),q1) = p
and
A2:
decomp (S,(len p),q2) = p
; q1 = q2
defpred S1[ Nat] means ( $1 <= len p implies (S ^^ $1) -head q1 = (S ^^ $1) -head q2 );
A3:
S1[ 0 ]
A10:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A11:
(
k <= len p implies
(S ^^ k) -head q1 = (S ^^ k) -head q2 )
;
S1[k + 1]
set r =
(S ^^ k) -head q1;
set s1 =
(S ^^ k) -tail q1;
set s2 =
(S ^^ k) -tail q2;
set t1 =
S -head ((S ^^ k) -tail q1);
set t2 =
S -head ((S ^^ k) -tail q2);
set u1 =
S -tail ((S ^^ k) -tail q1);
set u2 =
S -tail ((S ^^ k) -tail q2);
assume A12:
k + 1
<= len p
;
(S ^^ (k + 1)) -head q1 = (S ^^ (k + 1)) -head q2
1
<= k + 1
by NAT_1:11;
then A13:
k + 1
in Seg (len p)
by A12, FINSEQ_1:1;
then consider i being
Nat such that A14:
k + 1
= i + 1
and A15:
p . (k + 1) = S -head ((S ^^ i) -tail q1)
by A1, Def32;
consider j being
Nat such that A16:
k + 1
= j + 1
and A17:
p . (k + 1) = S -head ((S ^^ j) -tail q2)
by A2, A13, Def32;
k <= k + 1
by NAT_1:11;
then A18:
(S ^^ k) -head q1 = (S ^^ k) -head q2
by A11, A12, XXREAL_0:2;
(
q1 is
S ^^ k -headed &
(S ^^ k) -tail q1 is
S -headed )
by A12, Th22;
then
(
(S ^^ k) -head q1 in S ^^ k &
S -head ((S ^^ k) -tail q1) in S )
by Def9a;
then
((S ^^ k) -head q1) ^ (S -head ((S ^^ k) -tail q1)) in (S ^^ k) ^ S
by Def2;
then A20:
((S ^^ k) -head q1) ^ (S -head ((S ^^ k) -tail q1)) in S ^^ (k + 1)
by Th7;
q1 =
((S ^^ k) -head q1) ^ ((S ^^ k) -tail q1)
by Def10
.=
((S ^^ k) -head q1) ^ ((S -head ((S ^^ k) -tail q1)) ^ (S -tail ((S ^^ k) -tail q1)))
by Def10
.=
(((S ^^ k) -head q1) ^ (S -head ((S ^^ k) -tail q1))) ^ (S -tail ((S ^^ k) -tail q1))
by FINSEQ_1:32
;
then A21:
(S ^^ (k + 1)) -head q1 = ((S ^^ k) -head q1) ^ (S -head ((S ^^ k) -tail q1))
by A20, Th17;
(
q2 is
S ^^ k -headed &
(S ^^ k) -tail q2 is
S -headed )
by A12, Th22;
then
(
(S ^^ k) -head q1 in S ^^ k &
S -head ((S ^^ k) -tail q2) in S )
by A18, Def9a;
then
((S ^^ k) -head q1) ^ (S -head ((S ^^ k) -tail q2)) in (S ^^ k) ^ S
by Def2;
then A22:
((S ^^ k) -head q1) ^ (S -head ((S ^^ k) -tail q2)) in S ^^ (k + 1)
by Th7;
q2 =
((S ^^ k) -head q1) ^ ((S ^^ k) -tail q2)
by A18, Def10
.=
((S ^^ k) -head q1) ^ ((S -head ((S ^^ k) -tail q2)) ^ (S -tail ((S ^^ k) -tail q2)))
by Def10
.=
(((S ^^ k) -head q1) ^ (S -head ((S ^^ k) -tail q2))) ^ (S -tail ((S ^^ k) -tail q2))
by FINSEQ_1:32
;
then
(S ^^ (k + 1)) -head q2 = ((S ^^ k) -head q1) ^ (S -head ((S ^^ k) -tail q2))
by A22, Th17;
hence
(S ^^ (k + 1)) -head q1 = (S ^^ (k + 1)) -head q2
by A14, A15, A16, A17, A21;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A3, A10);
then A30:
(S ^^ (len p)) -head q1 = (S ^^ (len p)) -head q2
;
thus q1 =
(S ^^ (len p)) -head q1
by Th18
.=
q2
by A30, Th18
; verum