assume A1:
n <> 0
; 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;
( 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 )
;
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;
ex y being Element of bool the carrier of K st S1[i,x,y]
take
S *' x
;
S1[i,x,S *' x]
thus
S1[
i,
x,
S *' x]
;
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 RECDEF_1:sch 4(A2);
take
f /. (len f)
; 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
; ( 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; ( 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; ( 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; 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; ( i in dom f & i + 1 in dom f implies f . (i + 1) = S *' (f /. i) )
assume A6:
i in dom f
; ( not i + 1 in dom f or f . (i + 1) = S *' (f /. i) )
assume
i + 1 in dom f
; 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
S1[i,f . i,f . (i + 1)]
by A5, A7;
hence
f . (i + 1) = S *' (f /. i)
by A6, PARTFUN1:def 6; verum