A1
: (
product
(
rngs
u
)
c=
product
a
&
rng
(
Frege
u
)
=
product
(
rngs
u
)
)
by
Th14
,
FUNCT_6:38
;
(
dom
(
Frege
u
)
=
product
(
doms
u
)
&
doms
u
=
a
)
by
Th14
,
FUNCT_6:def 7
;
hence
Frege
u
is
UnOp
of
(
product
a
)
by
A1
,
FUNCT_2:def 1
,
RELSET_1:4
;
:: thesis:
verum