set n = len p;
let q1, q2 be Element of S ^^ (len p); :: thesis: ( 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 ; :: thesis: q1 = q2
defpred S₁[ Nat] means ( $1 <= len p implies (S ^^ $1) -head q1 = (S ^^ $1) -head q2 );
A3: S₁[ 0 ]

proof

assume 0 <= len p ; :: thesis: (S ^^ 0) -head q1 = (S ^^ 0) -head q2
thus (S ^^ 0) -head q1 = {} by Th58
.= (S ^^ 0) -head q2 by Th58 ; :: thesis: verum

end;

A10: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A11: ( k <= len p implies (S ^^ k) -head q1 = (S ^^ k) -head q2 ) ; :: thesis: S₁[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 ; :: thesis: (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, Th57;
then ( (S ^^ k) -head q1 in S ^^ k & S -head ((S ^^ k) -tail q1) in S ) by Def22;
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 Th6;
q1 = ((S ^^ k) -head q1) ^ ((S -head ((S ^^ k) -tail q1)) ^ (S -tail ((S ^^ k) -tail q1)))
.= (((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, Th52;
( q2 is S ^^ k -headed & (S ^^ k) -tail q2 is S -headed ) by A12, Th57;
then ( (S ^^ k) -head q1 in S ^^ k & S -head ((S ^^ k) -tail q2) in S ) by A18, Def22;
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 Th6;
q2 = ((S ^^ k) -head q1) ^ ((S -head ((S ^^ k) -tail q2)) ^ (S -tail ((S ^^ k) -tail q2))) by A18
.= (((S ^^ k) -head q1) ^ (S -head ((S ^^ k) -tail q2))) ^ (S -tail ((S ^^ k) -tail q2)) by FINSEQ_1:32 ;
hence (S ^^ (k + 1)) -head q1 = (S ^^ (k + 1)) -head q2 by A14, A15, A16, A17, A22, A21, Th52; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A10);
then (S ^^ (len p)) -head q1 = (S ^^ (len p)) -head q2 ;
hence q1 = q2 ; :: thesis: verum