dom
f
=
A
by
Th19
;
then
A1
:
f
.
a
in
rng
f
by
FUNCT_1:def 3
;
rng
f
c=
H
_{3}
(
G
)
by
Th19
;
hence
f
.
a
is
Element
of
G
by
A1
;
:: thesis:
verum