consider
f
being
Element
of
Funcs
V
,
A
,
B
being
Element
of
V
such that
A1
:
m
=
[
[
A
,
B
]
,
f
]
and
(
B
=
{}
implies
A
=
{}
)
and
f
is
Function
of
A
,
B
by
Th4
;
[
A
,
B
]
=
m
`1
by
A1
;
hence
(
m
`1
)
`1
is
Element
of
V
;
:: thesis:
verum