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

A2: 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;
A3: 0 + 1 <= i0 + 1 by XREAL_1:6;
i0 + 1 <= len s by A1, INT_1:58, NAT_1:13;
then i0 + 1 in dom s by A3, FINSEQ_3:25;
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
A4: ( 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(A2);
len p = len s by A4, 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 A4; :: thesis: verum