let H be LTL-formula; :: thesis: ex n being Nat ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = H & L . n = H & ( for k being Nat st 1 <= k & k < n holds
ex H1, F1 being LTL-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
take 1 ; :: thesis: ex L being FinSequence st
( 1 <= 1 & len L = 1 & L . 1 = H & L . 1 = H & ( for k being Nat st 1 <= k & k < 1 holds
ex H1, F1 being LTL-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
take <*H*> ; :: thesis: ( 1 <= 1 & len <*H*> = 1 & <*H*> . 1 = H & <*H*> . 1 = H & ( for k being Nat st 1 <= k & k < 1 holds
ex H1, F1 being LTL-formula st
( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus 1 <= 1 ; :: thesis: ( len <*H*> = 1 & <*H*> . 1 = H & <*H*> . 1 = H & ( for k being Nat st 1 <= k & k < 1 holds
ex H1, F1 being LTL-formula st
( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus len <*H*> = 1 by FINSEQ_1:40; :: thesis: ( <*H*> . 1 = H & <*H*> . 1 = H & ( for k being Nat st 1 <= k & k < 1 holds
ex H1, F1 being LTL-formula st
( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus ( <*H*> . 1 = H & <*H*> . 1 = H ) ; :: thesis: for k being Nat st 1 <= k & k < 1 holds
ex H1, F1 being LTL-formula st
( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
thus for k being Nat st 1 <= k & k < 1 holds
ex H1, F1 being LTL-formula st
( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ; :: thesis: verum