defpred S₁[ Nat, set , set ] means ex A, B being Element of LTLB_WFF st
( A = $2 & B = $3 & B = A '&&' (f /. ($1 + 1)) );

A1: now :: thesis: 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 S₁[n,x,y]

let n be Nat; :: thesis: ( 1 <= n & n < len f implies for x being Element of LTLB_WFF ex y being Element of LTLB_WFF st S₁[n,x,y] )
assume ( 1 <= n & n < len f ) ; :: thesis: for x being Element of LTLB_WFF ex y being Element of LTLB_WFF st S₁[n,x,y]
let x be Element of LTLB_WFF ; :: thesis: ex y being Element of LTLB_WFF st S₁[n,x,y]
S₁[n,x,x '&&' (f /. (n + 1))] ;
hence ex y being Element of LTLB_WFF st S₁[n,x,y] ; :: thesis: verum

end;

consider p being FinSequence of LTLB_WFF such that
A2: ( len p = len f & ( p . 1 = f /. 1 or len f = 0 ) & ( for n being Nat st 1 <= n & n < len f holds
S₁[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 & ( for i being Nat st 1 <= i & i < len f holds
p . (i + 1) = (p /. i) '&&' (f /. (i + 1)) ) ) ) :: thesis: ( not len f > 0 implies ex b₁ being FinSequence of LTLB_WFF st b₁ = <*TVERUM*> )

proof

A3: now :: thesis: for i being Nat st 1 <= i & i < len f holds
p . (i + 1) = (p /. i) '&&' (f /. (i + 1))

let i be Nat; :: thesis: ( 1 <= i & i < len f implies p . (i + 1) = (p /. i) '&&' (f /. (i + 1)) )
assume A4: ( 1 <= i & i < len f ) ; :: thesis: p . (i + 1) = (p /. i) '&&' (f /. (i + 1))
then ex A, B being Element of LTLB_WFF st
( A = p . i & B = p . (i + 1) & B = A '&&' (f /. (i + 1)) ) by A2;
hence p . (i + 1) = (p /. i) '&&' (f /. (i + 1)) by FINSEQ_4:15, A4, A2; :: thesis: verum

end;

assume len f > 0 ; :: thesis: ex p being FinSequence of LTLB_WFF st
( len p = len f & p . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds
p . (i + 1) = (p /. i) '&&' (f /. (i + 1)) ) )
then 1 <= len f by NAT_1:25;
hence ex p being FinSequence of LTLB_WFF st
( len p = len f & p . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds
p . (i + 1) = (p /. i) '&&' (f /. (i + 1)) ) ) by A3, A2, FINSEQ_4:15; :: thesis: verum

end;

thus ( not len f > 0 implies ex b₁ being FinSequence of LTLB_WFF st b₁ = <*TVERUM*> ) ; :: thesis: verum