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