let
f
,
g
be
Function
;
:: thesis:
for
A
being
set
holds
<:
f
,
g
:>

A
=
<:
f
,
(
g

A
)
:>
let
A
be
set
;
:: thesis:
<:
f
,
g
:>

A
=
<:
f
,
(
g

A
)
:>
thus
<:
f
,
g
:>

A
=
(
<:
g
,
f
:>
~
)

A
by
Th2
.=
(
<:
g
,
f
:>

A
)
~
by
Th3
.=
<:
(
g

A
)
,
f
:>
~
by
Th5
.=
<:
f
,
(
g

A
)
:>
by
Th2
;
:: thesis:
verum