consider x, y being object such that
x in LTLB_WFF ** and
y in LTLB_WFF ** and
A2: P = [x,y] by ZFMISC_1:def 2;
P `2 = [x,y] `2 by A2
.= y ;
hence P `2 is one-to-one FinSequence of LTLB_WFF by Def2; :: thesis: verum