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

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,('G' (f /. (n + 1))) => x] ;
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 = ('G' (f /. 1)) => A 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 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
p . (i + 1) = ('G' (f /. (i + 1))) => (p /. i) ) ) ) :: thesis: ( not len f > 0 implies ex b₁ being FinSequence of LTLB_WFF st b₁ = <*> LTLB_WFF )

proof

assume A3: len f > 0 ; :: thesis: ex p being FinSequence of LTLB_WFF st
( len p = len f & p . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
p . (i + 1) = ('G' (f /. (i + 1))) => (p /. i) ) )
take p ; :: thesis: ( len p = len f & p . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
p . (i + 1) = ('G' (f /. (i + 1))) => (p /. i) ) )

now :: thesis: for i being Element of NAT st 1 <= i & i < len f holds
p . (i + 1) = ('G' (f /. (i + 1))) => (p /. i)

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

end;

hence ( len p = len f & p . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
p . (i + 1) = ('G' (f /. (i + 1))) => (p /. i) ) ) by A2, A3; :: thesis: verum

end;

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