defpred S₁[ set ] means ex q being FinSequence of S ex r being Element of S ^^ (len q) st
( q = $1 & decomp (S,(len q),r) = q );
A1: S₁[ <*> S]

proof

take q = <*> S; :: thesis: ex r being Element of S ^^ (len q) st
( q = <*> S & decomp (S,(len q),r) = q )
reconsider r = {} as Element of S ^^ (len q) by Th4;
take r ; :: thesis: ( q = <*> S & decomp (S,(len q),r) = q )
thus ( q = <*> S & decomp (S,(len q),r) = q ) by Th61; :: thesis: verum

end;

A10: for s being FinSequence of S
for t being Element of S st S₁[s] holds
S₁[s ^ <*t*>]

proof

let s be FinSequence of S; :: thesis: for t being Element of S st S₁[s] holds
S₁[s ^ <*t*>]
let t be Element of S; :: thesis: ( S₁[s] implies S₁[s ^ <*t*>] )
set n = len s;
set q = s ^ <*t*>;
assume A11: S₁[s] ; :: thesis: S₁[s ^ <*t*>]
take s ^ <*t*> ; :: thesis: ex r being Element of S ^^ (len (s ^ <*t*>)) st
( s ^ <*t*> = s ^ <*t*> & decomp (S,(len (s ^ <*t*>)),r) = s ^ <*t*> )
consider q1 being FinSequence of S such that
A12: ex r1 being Element of S ^^ (len q1) st
( q1 = s & decomp (S,(len q1),r1) = q1 ) by A11;
consider r1 being Element of S ^^ (len q1) such that
A13: q1 = s and
A14: decomp (S,(len q1),r1) = q1 by A12;
set r = r1 ^ t;
A15: len (s ^ <*t*>) = (len s) + (len <*t*>) by FINSEQ_1:22
.= (len s) + 1 by FINSEQ_1:39 ;
r1 ^ t in (S ^^ (len s)) ^ S by A13, Def2;
then reconsider r = r1 ^ t as Element of S ^^ (len (s ^ <*t*>)) by A15, Th6;
take r ; :: thesis: ( s ^ <*t*> = s ^ <*t*> & decomp (S,(len (s ^ <*t*>)),r) = s ^ <*t*> )
thus s ^ <*t*> = s ^ <*t*> ; :: thesis: decomp (S,(len (s ^ <*t*>)),r) = s ^ <*t*>
set q2 = decomp (S,(len (s ^ <*t*>)),r);
A20: len (decomp (S,(len (s ^ <*t*>)),r)) = len (s ^ <*t*>) by Th62;
for k being Nat st 1 <= k & k <= len (s ^ <*t*>) holds
(s ^ <*t*>) . k = (decomp (S,(len (s ^ <*t*>)),r)) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (s ^ <*t*>) implies (s ^ <*t*>) . k = (decomp (S,(len (s ^ <*t*>)),r)) . k )
assume that
A21: 1 <= k and
A22: k <= len (s ^ <*t*>) ; :: thesis: (s ^ <*t*>) . k = (decomp (S,(len (s ^ <*t*>)),r)) . k
k in Seg (len (s ^ <*t*>)) by A21, A22, FINSEQ_1:1;
then consider i being Nat such that
A23: k = i + 1 and
A24: (decomp (S,(len (s ^ <*t*>)),r)) . k = S -head ((S ^^ i) -tail r) by Def32;

per cases ( k <= len s or k > len s ) ;

suppose A30: k <= len s ; :: thesis: (s ^ <*t*>) . k = (decomp (S,(len (s ^ <*t*>)),r)) . k

then A31: k in Seg (len s) by A21, FINSEQ_1:1;
then consider j being Nat such that
A32: k = j + 1 and
A33: q1 . k = S -head ((S ^^ j) -tail r1) by A13, A14, Def32;
A34: k in dom s by A31, FINSEQ_1:def 3;
A35: ( r1 is S ^^ i -headed & (S ^^ i) -tail r1 is S -headed ) by A13, A23, A30, Th57;
then A36: (S ^^ i) -tail r = ((S ^^ i) -tail r1) ^ t by Th56;
thus (s ^ <*t*>) . k = S -head ((S ^^ i) -tail r1) by A13, A23, A32, A33, A34, FINSEQ_1:def 7
.= (decomp (S,(len (s ^ <*t*>)),r)) . k by A24, A35, A36, Th56 ; :: thesis: verum

end;

suppose k > len s ; :: thesis: (s ^ <*t*>) . k = (decomp (S,(len (s ^ <*t*>)),r)) . k

then k = (len s) + 1 by A15, A22, NAT_1:8;
hence (s ^ <*t*>) . k = (decomp (S,(len (s ^ <*t*>)),r)) . k by A13, A23, A24, FINSEQ_1:42; :: thesis: verum

end;

end;

end;

hence decomp (S,(len (s ^ <*t*>)),r) = s ^ <*t*> by A20; :: thesis: verum

end;

for q being FinSequence of S holds S₁[q] from FINSEQ_2:sch 2(A1, A10);
then S₁[p] ;
hence ex b₁ being Element of S ^^ (len p) st decomp (S,(len p),b₁) = p ; :: thesis: verum