theorem :: FIELD_7:43

for F being Field
for E being FieldExtension of F
for K being FieldExtension of E holds F_Alg K is FieldExtension of F_Alg E