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