theorem lift9: :: FIELD_12:37

for F1, F2 being Field
for E being FieldExtension of F1 st F1 == F2 holds
E is FieldExtension of F2