theorem lemNor1cu: :: FIELD_13:11

for F being Field
for E1 being FieldExtension of F
for E2 being Field st E1 == E2 holds
E2 is FieldExtension of F