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