let A be Element of LTLB_WFF ; :: thesis: (con <*A*>) /. (len (con <*A*>)) = A
set f = <*A*>;
A1: len <*A*> = 1 by FINSEQ_1:39;
thus H₂(<*A*>) = (con <*A*>) /. (len <*A*>) by Def2
.= <*A*> /. 1 by Th6, A1
.= A by FINSEQ_4:16 ; :: thesis: verum