let
K
be
Field
;
:: thesis:
K
is
Subfield
of
K
A1
: the
addF
of
K
=
the
addF
of
K
||
the
carrier
of
K
;
A2
: the
multF
of
K
=
the
multF
of
K
||
the
carrier
of
K
;
( the
carrier
of
K
c=
the
carrier
of
K
&
1.
K
=
1.
K
&
0.
K
=
0.
K
) ;
hence
K
is
Subfield
of
K
by
A1
,
A2
,
EC_PF_1:def 1
;
:: thesis:
verum