reconsider
ab
=
[
a
,
b
]
as
Element
of
[:
A
,
B
:]
by
ZFMISC_1:def 2
;
f
.
ab
is
Element
of
C
;
hence
f
.
(
a
,
b
) is
Element
of
C
;
:: thesis:
verum