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 :: 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 S1[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 S1[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 S1[n,x,y]
let x be Element of LTLB_WFF ; :: thesis: 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] ; :: thesis: 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 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) ) ) ) :: thesis: ( not len f > 0 implies ex b1 being FinSequence of LTLB_WFF st b1 = <*> LTLB_WFF )
proof
assume A3: len f > 0 ; :: thesis: 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) ) )

take p ; :: thesis: ( 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) ) )

now :: thesis: for i being Element of NAT st 1 <= i & i < len f holds
p . (i + 1) = (f /. (i + 1)) => (p /. i)
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len f implies p . (i + 1) = (f /. (i + 1)) => (p /. i) )
assume A4: ( 1 <= i & i < len f ) ; :: thesis: p . (i + 1) = (f /. (i + 1)) => (p /. i)
then ex A, B being Element of LTLB_WFF st
( A = p . i & B = p . (i + 1) & B = (f /. (i + 1)) => A ) by A2;
hence p . (i + 1) = (f /. (i + 1)) => (p /. i) by ; :: thesis: verum
end;
hence ( 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) ) ) by A2, A3; :: thesis: verum
end;
thus ( not len f > 0 implies ex b1 being FinSequence of LTLB_WFF st b1 = <*> LTLB_WFF ) ; :: thesis: verum