hereby :: thesis: ( not n = 0 implies ex b1 being Subset of K ex f being FinSequence of bool the carrier of K st
( b1 = 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 bool 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 b1 being Subset of K ex f being FinSequence of bool the carrier of K st
( b1 = 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 S1[ 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 S1[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 S1[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 S1[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 S1[i,x,y]
take S *' x ; :: thesis: S1[i,x,S *' x]
thus S1[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
S1[i,f . i,f . (i + 1)] from 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 ;
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 ;
then A7: i < n1 by NAT_1:13;
1 <= i by ;
then S1[i,f . i,f . (i + 1)] by A5, A7;
hence f . (i + 1) = S *' (f /. i) by ; :: thesis: verum