theorem lift3: :: FIELD_12:62

for F being Field
for L being b₁ -homomorphic b₁ -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