theorem FAutEQ: :: FIELD_16:15

for F being Field
for E1, E2 being FieldExtension of F st E1 == E2 holds
{ f where f is Automorphism of E1 : verum } = { f where f is Automorphism of E2 : verum }