theorem FAutEQ1: :: FIELD_16:14

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