let F be Field; for A1, A2 being AlgebraicClosure of F holds A1,A2 are_isomorphic_over F
let E1, E2 be AlgebraicClosure of F; E1,E2 are_isomorphic_over F
reconsider L = E2 as algebraic-closed F -homomorphic F -monomorphic Field ;
reconsider f = id F as Monomorphism of F,L by lift5a;
consider g being Function of E1,L such that
A:
( g is monomorphism & g is f -extending )
by lift2;
C:
doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) == F
by lemug1;
Image f = doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #)
proof
set If =
Image f;
H:
F is
Subfield of
E2
by FIELD_4:7;
B: the
carrier of
(Image f) =
rng f
by RING_2:def 6
.=
the
carrier of
F
;
C: the
addF of
(Image f) =
the
addF of
L || (rng f)
by RING_2:def 6
.=
the
addF of
F
by H, EC_PF_1:def 1
;
D: the
multF of
(Image f) =
the
multF of
L || (rng f)
by RING_2:def 6
.=
the
multF of
F
by H, EC_PF_1:def 1
;
E: the
OneF of
(Image f) =
1. L
by RING_2:def 6
.=
1. F
by H, EC_PF_1:def 1
;
the
ZeroF of
(Image f) =
0. L
by RING_2:def 6
.=
0. F
by H, EC_PF_1:def 1
;
hence
Image f = doubleLoopStr(# the
carrier of
F, the
addF of
F, the
multF of
F, the
OneF of
F, the
ZeroF of
F #)
by B, C, D, E;
verum
end;
then
L is AlgebraicClosure of Image f
by C, lift4;
then B:
g is isomorphism
by A, lift3;
then
g is F -fixing
;
hence
E1,E2 are_isomorphic_over F
by B, FIELD_8:def 5; verum