hereby :: thesis: ( not n = 0 implies ex b_{1} being Subset of K ex f being FinSequence of bool the carrier of K st

( b_{1} = 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 A1:
n <> 0
; :: thesis: ex b( b

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;take A = [#] K; :: thesis: A = the carrier of K

thus A = the carrier of K ; :: thesis: verum

( b

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

( 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

proof

consider f being FinSequence of bool the carrier of K such that
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_{1}[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_{1}[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_{1}[i,x,y]

take S *' x ; :: thesis: S_{1}[i,x,S *' x]

thus S_{1}[i,x,S *' x]
; :: thesis: verum

end;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

let x be Element of bool the carrier of K; :: thesis: ex y being Element of bool the carrier of K st S

take S *' x ; :: thesis: S

thus S

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

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 A7: i < n1 by NAT_1:13;

1 <= i by A6, FINSEQ_3:25;

then S

hence f . (i + 1) = S *' (f /. i) by A6, PARTFUN1:def 6; :: thesis: verum