let F be Field; :: thesis: for E being FieldExtension of F
for E1, E2 being b₁ -extending FieldExtension of F
for h being Function of E1,E2 st h is E -fixing holds
h is F -fixing
let E be FieldExtension of F; :: thesis: for E1, E2 being E -extending FieldExtension of F
for h being Function of E1,E2 st h is E -fixing holds
h is F -fixing
let E1, E2 be E -extending FieldExtension of F; :: thesis: for h being Function of E1,E2 st h is E -fixing holds
h is F -fixing
let h be Function of E1,E2; :: thesis: ( h is E -fixing implies h is F -fixing )
assume AS: h is E -fixing ; :: thesis: h is F -fixing

now :: thesis: for a being Element of F holds h . a = a

let a be Element of F; :: thesis: h . a = a
thus h . a = h . (@ (a,E)) by FIELD_7:def 4
.= @ (a,E) by AS
.= a by FIELD_7:def 4 ; :: thesis: verum

end;

hence h is F -fixing ; :: thesis: verum