let F be Field; :: thesis: for E being FieldExtension of F holds MultGroup F is Subgroup of MultGroup E
let E be FieldExtension of F; :: thesis: MultGroup F is Subgroup of MultGroup E
set M1 = MultGroup E;
set M2 = MultGroup F;
H0: F is Subfield of E by FIELD_4:7;
H2: {(0. E)} = {(0. F)} by H0, EC_PF_1:def 1;
the carrier of F c= the carrier of E by H0, EC_PF_1:def 1;
then NonZero F c= NonZero E by H2, XBOOLE_1:33;
then NonZero F c= the carrier of (MultGroup E) by UNIROOTS:def 1;
then A: the carrier of (MultGroup F) c= the carrier of (MultGroup E) by UNIROOTS:def 1;
then H3: [: the carrier of (MultGroup F), the carrier of (MultGroup F):] c= [: the carrier of (MultGroup E), the carrier of (MultGroup E):] by ZFMISC_1:96;
the carrier of (MultGroup F) c= the carrier of F by UNIROOTS:20;
then H4: [: the carrier of (MultGroup F), the carrier of (MultGroup F):] c= [: the carrier of F, the carrier of F:] by ZFMISC_1:96;
the multF of (MultGroup E) || the carrier of (MultGroup F) = ( the multF of E || the carrier of (MultGroup E)) || the carrier of (MultGroup F) by UNIROOTS:def 1
.= the multF of E || the carrier of (MultGroup F) by H3, FUNCT_1:51
.= ( the multF of E || the carrier of F) || the carrier of (MultGroup F) by H4, FUNCT_1:51
.= the multF of F || the carrier of (MultGroup F) by H0, EC_PF_1:def 1
.= the multF of (MultGroup F) by UNIROOTS:def 1 ;
hence MultGroup F is Subgroup of MultGroup E by A, GROUP_2:def 5; :: thesis: verum