let F be Field; :: thesis: for E1, E2 being FieldExtension of F st E1 == E2 holds
for f being Automorphism of E1 holds f is Automorphism of E2
let E1, E2 be FieldExtension of F; :: thesis: ( E1 == E2 implies for f being Automorphism of E1 holds f is Automorphism of E2 )
assume AS: E1 == E2 ; :: thesis: for f being Automorphism of E1 holds f is Automorphism of E2
let f be Automorphism of E1; :: thesis: f is Automorphism of E2
reconsider g = f as Function of E2,E2 by AS;

now :: thesis: for a1, a2 being Element of E2 holds g . (a1 + a2) = (g . a1) + (g . a2)

let a1, a2 be Element of E2; :: thesis: g . (a1 + a2) = (g . a1) + (g . a2)
reconsider b1 = a1, b2 = a2 as Element of E1 by AS;
thus g . (a1 + a2) = f . (b1 + b2) by AS
.= (f . b1) + (f . b2) by VECTSP_1:def 20
.= (g . a1) + (g . a2) by AS ; :: thesis: verum

end;

then B: g is additive ;

now :: thesis: for a1, a2 being Element of E2 holds g . (a1 * a2) = (g . a1) * (g . a2)

let a1, a2 be Element of E2; :: thesis: g . (a1 * a2) = (g . a1) * (g . a2)
reconsider b1 = a1, b2 = a2 as Element of E1 by AS;
thus g . (a1 * a2) = f . (b1 * b2) by AS
.= (f . b1) * (f . b2) by GROUP_6:def 6
.= (g . a1) * (g . a2) by AS ; :: thesis: verum

end;

then C: g is multiplicative ;
g . (1_ E2) = f . (1_ E1) by AS
.= 1_ E2 by AS, GROUP_1:def 13 ;
then g is unity-preserving ;
hence f is Automorphism of E2 by AS, B, C; :: thesis: verum