A1: len (<*> LTLB_WFF) = 0 ;
then con (<*> LTLB_WFF) = <*TVERUM*> by Def2;
then A2: len (con (<*> LTLB_WFF)) = 1 by FINSEQ_1:39;
hence H₂( <*> LTLB_WFF) = (con (<*> LTLB_WFF)) . (len (con (<*> LTLB_WFF))) by FINSEQ_4:15
.= <*TVERUM*> . (len (con (<*> LTLB_WFF))) by Def2, A1
.= TVERUM by A2 ;
:: thesis: verum