for F being Field
for E1, E2, E3 being FieldExtension of F st E1,E2 are_isomorphic_over F & E2,E3 are_isomorphic_over F holds
E1,E3 are_isomorphic_over F