let F be Field; :: thesis: for L being F -homomorphic F -monomorphic Field
for A being AlgebraicClosure of F
for f being Monomorphism of F,L st L is AlgebraicClosure of Image f holds
for g being Function of A,L st g is monomorphism & g is f -extending holds
g is isomorphism
let L be F -homomorphic F -monomorphic Field; :: thesis: for A being AlgebraicClosure of F
for f being Monomorphism of F,L st L is AlgebraicClosure of Image f holds
for g being Function of A,L st g is monomorphism & g is f -extending holds
g is isomorphism
let E be AlgebraicClosure of F; :: thesis: for f being Monomorphism of F,L st L is AlgebraicClosure of Image f holds
for g being Function of E,L st g is monomorphism & g is f -extending holds
g is isomorphism
let f be Monomorphism of F,L; :: thesis: ( L is AlgebraicClosure of Image f implies for g being Function of E,L st g is monomorphism & g is f -extending holds
g is isomorphism )
assume AS1: L is AlgebraicClosure of Image f ; :: thesis: for g being Function of E,L st g is monomorphism & g is f -extending holds
g is isomorphism
let g be Function of E,L; :: thesis: ( g is monomorphism & g is f -extending implies g is isomorphism )
assume AS2: ( g is monomorphism & g is f -extending ) ; :: thesis: g is isomorphism
then reconsider L1 = L as E -homomorphic E -monomorphic Field by RING_3:def 3, RING_2:def 4;
reconsider g1 = g as Monomorphism of E,L1 by AS2;
B: Image g1 is algebraic-closed by lift3c;
reconsider If = Image f as Field ;
If is Subfield of Image g1 by AS2, lift3b;
then reconsider Ig = Image g1 as FieldExtension of If by FIELD_4:7;
reconsider L1 = L1 as FieldExtension of If by AS1;
Ig is Subring of L1 by FIELD_5:12;
then reconsider L1 = L1 as Ig -extending FieldExtension of If by FIELD_4:def 1;
L1 is If -algebraic by AS1;
then Ig is AlgebraicClosure of If by B, defAC, FIELD_7:40;
then doubleLoopStr(# the carrier of L1, the addF of L1, the multF of L1, the OneF of L1, the ZeroF of L1 #) = doubleLoopStr(# the carrier of Ig, the addF of Ig, the multF of Ig, the OneF of Ig, the ZeroF of Ig #) by AS1, lift3a, FIELD_7:def 1;
then g is onto by RING_2:def 6;
hence g is isomorphism by AS2; :: thesis: verum