defpred S₁[ Nat, set ] means $2 = s . (((($1 - 1) + n) mod (len s)) + 1);

P1: now :: thesis: for k being Nat st k in Seg (len s) holds
ex x being Element of D st S₁[k,x]

let k be Nat; :: thesis: ( k in Seg (len s) implies ex x being Element of D st S₁[k,x] )
assume k in Seg (len s) ; :: thesis: ex x being Element of D st S₁[k,x]
reconsider i0 = ((k - 1) + n) mod (len s) as Element of NAT by INT_1:3, INT_1:57;
P21: 0 + 1 <= i0 + 1 by XREAL_1:6;
((k - 1) + n) mod (len s) < len s by AS, INT_1:58;
then i0 + 1 <= len s by NAT_1:13;
then i0 + 1 in Seg (len s) by P21;
then i0 + 1 in dom s by FINSEQ_1:def 3;
then s . (i0 + 1) in D by FINSEQ_2:11;
hence ex x being Element of D st S₁[k,x] ; :: thesis: verum

end;

consider p being FinSequence of D such that
P3: ( dom p = Seg (len s) & ( for k being Nat st k in Seg (len s) holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 5(P1);
len p = len s by P3, FINSEQ_1:def 3;
hence ex b₁ being FinSequence of D st
( len b₁ = len s & ( for i being Nat st i in Seg (len s) holds
b₁ . i = s . ((((i - 1) + n) mod (len s)) + 1) ) ) by P3; :: thesis: verum