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