let
R
be
Skew-Field
;
:: thesis:
the
carrier
of
R
=
the
carrier
of
(
MultGroup
R
)
\/
{
(
0.
R
)
}
NonZero
R
=
the
carrier
of
(
MultGroup
R
)
by
Def1
;
hence
the
carrier
of
R
=
the
carrier
of
(
MultGroup
R
)
\/
{
(
0.
R
)
}
by
XBOOLE_1:45
;
:: thesis:
verum