hereby :: thesis: ( not n = 0 implies ex b₁ being Subset of K ex f being FinSequence of bool the carrier of K st
( b₁ = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = S *' (f /. i) ) ) )

assume n = 0 ; :: thesis: ex A being Element of K10( the carrier of K) st A = the carrier of K
take A = [#] K; :: thesis: A = the carrier of K
thus A = the carrier of K ; :: thesis: verum

end;

assume A1: n <> 0 ; :: thesis: ex b₁ being Subset of K ex f being FinSequence of bool the carrier of K st
( b₁ = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = S *' (f /. i) ) )
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]

proof

let i be Nat; :: thesis: ( 1 <= i & i < n1 implies 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] )
assume ( 1 <= i & i < n1 ) ; :: thesis: 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 x be Element of bool the carrier of K; :: thesis: ex y being Element of bool the carrier of K st S₁[i,x,y]
take S *' x ; :: thesis: S₁[i,x,S *' x]
thus S₁[i,x,S *' x] ; :: thesis: verum

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: ex f being FinSequence of bool the carrier of K st
( f /. (len f) = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = S *' (f /. i) ) )
take f ; :: thesis: ( f /. (len f) = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = S *' (f /. i) ) )
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: ( len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = S *' (f /. i) ) )
thus len f = n by A3; :: thesis: ( f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = S *' (f /. i) ) )
thus f . 1 = S by A1, A4; :: thesis: for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = S *' (f /. i)
let i be Nat; :: thesis: ( i in dom f & i + 1 in dom f implies f . (i + 1) = S *' (f /. i) )
assume A6: i in dom f ; :: thesis: ( not i + 1 in dom f or f . (i + 1) = S *' (f /. i) )
assume i + 1 in dom f ; :: thesis: f . (i + 1) = S *' (f /. i)
then i + 1 <= n1 by A3, FINSEQ_3:25;
then i < n1 by NAT_1:13;
then S₁[i,f . i,f . (i + 1)] by A6, FINSEQ_3:25, A5;
hence f . (i + 1) = S *' (f /. i) by A6, PARTFUN1:def 6; :: thesis: verum