theorem MGsub: :: FIELD_15:9

for F being Field
for E being FieldExtension of F holds MultGroup F is Subgroup of MultGroup E