defpred S₁[ object , object ] means ex k being Nat st
( $1 = k + 1 & $2 = S -head ((S ^^ k) -tail p) );
A1: for i being Nat st i in Seg n holds
ex s being Element of S st S₁[i,s]

proof

let i be Nat; :: thesis: ( i in Seg n implies ex s being Element of S st S₁[i,s] )
assume i in Seg n ; :: thesis: ex s being Element of S st S₁[i,s]
then A3: ( 1 <= i & i <= n ) by FINSEQ_1:1;
then consider j being Nat such that
A4: i = j + 1 by NAT_1:6;
consider l being Nat such that
A5: i + l = n by A3, NAT_1:10;
reconsider p = p as Element of S ^^ ((j + 1) + l) by A4, A5;
take decomp (S,j,l,p) ; :: thesis: S₁[i, decomp (S,j,l,p)]
thus S₁[i, decomp (S,j,l,p)] by A4; :: thesis: verum

end;

consider q being FinSequence of S such that
A10: dom q = Seg n and
A11: for i being Nat st i in Seg n holds
S₁[i,q . i] from FINSEQ_1:sch 5(A1);
take q ; :: thesis: ( dom q = Seg n & ( for m being Nat st m in Seg n holds
ex k being Nat st
( m = k + 1 & q . m = S -head ((S ^^ k) -tail p) ) ) )
thus ( dom q = Seg n & ( for m being Nat st m in Seg n holds
ex k being Nat st
( m = k + 1 & q . m = S -head ((S ^^ k) -tail p) ) ) ) by A10, A11; :: thesis: verum