end;

assume A1: n <> 0 ; :: thesis:
set D = bool the carrier of K;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
defpred S₁[ set , set , set ] means ex A being Subset of K st
( A = $2 & $3 = S *' A );
A2: for i being Nat st 1 <= i & i < n1 holds
for x being Element of bool the carrier of K ex y being Element of bool the carrier of K st S₁[i,x,y]

let i be Nat; :: thesis:
assume ( 1 <= i & i < n1 ) ; :: thesis:
let x be Element of bool the carrier of K; :: thesis:
take S *' x ; :: thesis:
thus S₁[i,x,S *' x] ; :: thesis:

end;

consider f being FinSequence of bool the carrier of K such that
A3: len f = n1 and
A4: ( f . 1 = S or n1 = 0 ) and
A5: for i being Nat st 1 <= i & i < n1 holds
S₁[i,f . i,f . (i + 1)] from RECDEF_1:sch 4(A2);
take f /. (len f) ; :: thesis:
take f ; :: thesis:
len f in dom f by A1, A3, CARD_1:27, FINSEQ_5:6;
hence f /. (len f) = f . (len f) by PARTFUN1:def 6; :: thesis:
thus len f = n by A3; :: thesis:
thus f . 1 = S by A1, A4; :: thesis:
let i be Nat; :: thesis:
assume A6: i in dom f ; :: thesis:
assume i + 1 in dom f ; :: thesis:
then i + 1 <= n1 by A3, FINSEQ_3:25;
then A7: i < n1 by NAT_1:13;
1 <= i by A6, FINSEQ_3:25;
then S₁[i,f . i,f . (i + 1)] by A5, A7;
hence f . (i + 1) = S *' (f /. i) by A6, PARTFUN1:def 6; :: thesis: