let H be LTL-formula; :: thesis: ( H is disjunctive implies H . 1 = 2 )
assume H is disjunctive ; :: thesis: H . 1 = 2
then consider F, G being LTL-formula such that
A1: H = F 'or' G by Def17;
( H = (<*2*> ^ F) ^ G & (<*2*> ^ F) ^ G = <*2*> ^ (F ^ G) ) by A1, FINSEQ_1:45;
hence H . 1 = 2 by FINSEQ_1:58; :: thesis: verum