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