let F be Field; :: thesis: for E being F -algebraic FieldExtension of F
for h being F -fixing Monomorphism of E holds h is Automorphism of E
let E be F -algebraic FieldExtension of F; :: thesis: for h being F -fixing Monomorphism of E holds h is Automorphism of E
let h be F -fixing Monomorphism of E; :: thesis: h is Automorphism of E
( the carrier of E c= rng h & rng h c= the carrier of E ) by fixr, RELAT_1:def 19;
then h is onto by XBOOLE_0:def 10;
hence h is Automorphism of E ; :: thesis: verum