let H be LTL-formula; :: thesis: ( H is Release implies H . 1 = 5 )
assume H is Release ; :: thesis: H . 1 = 5
then consider F, G being LTL-formula such that
A1: H = F 'R' G ;
(<*5*> ^ F) ^ G = <*5*> ^ (F ^ G) by FINSEQ_1:32;
hence H . 1 = 5 by A1, FINSEQ_1:41; :: thesis: verum