let f be FinSequence of LTLB_WFF ; :: thesis: ( len f > 0 implies (con f) /. 1 = f /. 1 )
assume A1: len f > 0 ; :: thesis: (con f) /. 1 = f /. 1
then A2: 1 <= len f by NAT_1:25;
then len (con f) >= 1 by Def2;
hence (con f) /. 1 = (con f) . 1 by FINSEQ_4:15
.= f . 1 by Def2, A1
.= f /. 1 by FINSEQ_4:15, A2 ;
:: thesis: verum