defpred S1[ Nat, set , set ] means ex A, B being Element of LTLB_WFF st
( A = $2 & B = $3 & B = (f /. ($1 + 1)) => A );
A1:
now for n being Nat st 1 <= n & n < len f holds
for x being Element of LTLB_WFF ex y being Element of LTLB_WFF st S1[n,x,y]let n be
Nat;
( 1 <= n & n < len f implies for x being Element of LTLB_WFF ex y being Element of LTLB_WFF st S1[n,x,y] )assume
( 1
<= n &
n < len f )
;
for x being Element of LTLB_WFF ex y being Element of LTLB_WFF st S1[n,x,y]let x be
Element of
LTLB_WFF ;
ex y being Element of LTLB_WFF st S1[n,x,y]
S1[
n,
x,
(f /. (n + 1)) => x]
;
hence
ex
y being
Element of
LTLB_WFF st
S1[
n,
x,
y]
;
verum end;
consider p being FinSequence of LTLB_WFF such that
A2:
( len p = len f & ( p . 1 = (f /. 1) => A or len f = 0 ) & ( for n being Nat st 1 <= n & n < len f holds
S1[n,p . n,p . (n + 1)] ) )
from RECDEF_1:sch 4(A1);
thus
( len f > 0 implies ex p being FinSequence of LTLB_WFF st
( len p = len f & p . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
p . (i + 1) = (f /. (i + 1)) => (p /. i) ) ) )
( not len f > 0 implies ex b1 being FinSequence of LTLB_WFF st b1 = <*> LTLB_WFF )
thus
( not len f > 0 implies ex b1 being FinSequence of LTLB_WFF st b1 = <*> LTLB_WFF )
; verum