let H be LTL-formula; :: thesis: ( <*H*> . 1 = H & rng <*H*> = {H} )
set p = <*H*>;
( dom <*H*> = {1} & <*H*> . 1 = H ) by FINSEQ_1:2, FINSEQ_1:def 8;
hence ( <*H*> . 1 = H & rng <*H*> = {H} ) by FUNCT_1:4; :: thesis: verum