:: Existence and Uniqueness of Algebraic Closures
:: by Christoph Schwarzweller
::
:: Received December 27, 2022
:: Copyright (c) 2022-2025 Association of Mizar Users


registration
let L be non empty doubleLoopStr ;
cluster doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) -> non empty ;
coherence
not doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is empty ;
end;

registration
let L be non trivial doubleLoopStr ;
cluster doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) -> non trivial ;
coherence
not doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is trivial ;
end;

registration
let L be non degenerated doubleLoopStr ;
cluster doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) -> non degenerated ;
coherence
not doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is degenerated
proof end;
end;

registration
let L be add-associative doubleLoopStr ;
cluster doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) -> add-associative ;
coherence
doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is add-associative
proof end;
end;

registration
let L be right_zeroed doubleLoopStr ;
cluster doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) -> right_zeroed ;
coherence
doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is right_zeroed
proof end;
end;

registration
let L be right_complementable doubleLoopStr ;
cluster doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) -> right_complementable ;
coherence
doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is right_complementable
proof end;
end;

registration
let L be Abelian doubleLoopStr ;
cluster doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) -> Abelian ;
coherence
doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is Abelian
proof end;
end;

registration
let L be associative doubleLoopStr ;
cluster doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) -> associative ;
coherence
doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is associative
proof end;
end;

registration
let L be non empty well-unital doubleLoopStr ;
cluster doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) -> well-unital ;
coherence
doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is well-unital
proof end;
end;

registration
let L be non empty left-distributive doubleLoopStr ;
cluster doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) -> left-distributive ;
coherence
doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is left-distributive
proof end;
end;

registration
let L be non empty right-distributive doubleLoopStr ;
cluster doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) -> right-distributive ;
coherence
doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is right-distributive
proof end;
end;

registration
let L be commutative doubleLoopStr ;
cluster doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) -> commutative ;
coherence
doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is commutative
proof end;
end;

registration
let L be non empty domRing-like doubleLoopStr ;
cluster doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) -> domRing-like ;
coherence
doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is domRing-like
proof end;
end;

registration
let L be almost_left_invertible doubleLoopStr ;
cluster doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) -> almost_left_invertible ;
coherence
doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is almost_left_invertible
proof end;
end;

lemug: for F being Field holds doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) is Subfield of F
proof end;

theorem lemug1: :: FIELD_12:1
for F being Field holds doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) == F
proof end;

registration
let F be Field;
cluster non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible strict Abelian add-associative right_zeroed zeroed right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like gcd-like PID Euclidian Polynom-Ring F -homomorphic factorial F -extending for doubleLoopStr ;
existence
ex b1 being FieldExtension of F st b1 is strict
proof end;
end;

registration
let F be Field;
let L be F -monomorphic Field;
cluster non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible Abelian add-associative right_zeroed zeroed right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like gcd-like PID Euclidian F -homomorphic Polynom-Ring L -homomorphic factorial F -monomorphic L -extending for doubleLoopStr ;
existence
ex b1 being FieldExtension of L st
( b1 is F -homomorphic & b1 is F -monomorphic )
proof end;
end;

registration
let F be Field;
cluster non empty Relation-like NAT -defined the carrier of F -valued Function-like total quasi_total left_complementable right_complementable complementable finite-Support monic irreducible for Element of the carrier of (Polynom-Ring F);
existence
ex b1 being Element of the carrier of (Polynom-Ring F) st
( b1 is monic & b1 is irreducible )
proof end;
end;

registration
let F be non algebraic-closed Field;
cluster non empty Relation-like NAT -defined the carrier of F -valued Function-like total quasi_total left_complementable right_complementable complementable finite-Support monic non with_roots non constant for Element of the carrier of (Polynom-Ring F);
existence
ex b1 being Element of the carrier of (Polynom-Ring F) st
( b1 is monic & not b1 is constant & not b1 is with_roots )
proof end;
end;

theorem F815: :: FIELD_12:2
for F1 being Field
for F2 being b1 -homomorphic b1 -monomorphic Field
for h being Monomorphism of F1,F2
for p being Element of the carrier of (Polynom-Ring F1) holds (PolyHom h) . (- p) = - ((PolyHom h) . p)
proof end;

theorem F814: :: FIELD_12:3
for F1 being Field
for F2 being b1 -homomorphic b1 -monomorphic Field
for h being Monomorphism of F1,F2
for p, q being Element of the carrier of (Polynom-Ring F1) st p divides q holds
(PolyHom h) . p divides (PolyHom h) . q
proof end;

registration
let F1 be Field;
let F2 be F1 -homomorphic F1 -monomorphic Field;
let h be Monomorphism of F1,F2;
let p be non constant Element of the carrier of (Polynom-Ring F1);
cluster (PolyHom h) . p -> non constant for Element of the carrier of (Polynom-Ring F2);
coherence
for b1 being Element of the carrier of (Polynom-Ring F2) st b1 = (PolyHom h) . p holds
not b1 is constant
proof end;
end;

definition
let R be gcdDomain;
let a, b be Element of R;
pred a,b are_coprime means :: FIELD_12:def 1
 1. R is a_gcd of a,b;
end;

:: deftheorem defines are_coprime FIELD_12:def 1 :
for R being gcdDomain
for a, b being Element of R holds
( a,b are_coprime iff 1. R is a_gcd of a,b );

theorem copr1: :: FIELD_12:4
for F being Field
for p, q being Element of the carrier of (Polynom-Ring F) holds
( p,q are_coprime iff p gcd q = 1_. F )
proof end;

theorem copr2: :: FIELD_12:5
for F being Field
for p, q being Element of the carrier of (Polynom-Ring F) st p,q are_coprime holds
p,q have_no_common_roots
proof end;

theorem mi1: :: FIELD_12:6
for F being Field
for p being Element of the carrier of (Polynom-Ring F) holds
( ex E being FieldExtension of F ex a being b1 -algebraic Element of E st p = MinPoly (a,F) iff ( p is monic & p is irreducible ) )
proof end;

theorem mi2: :: FIELD_12:7
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F) ex E being b1 -finite FieldExtension of F st
( deg (E,F) = deg p & p is_with_roots_in E )
proof end;

theorem :: FIELD_12:8
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F) ex E being b1 -finite FieldExtension of F st
( p is_with_roots_in E & deg (E,F) <= deg p )
proof end;

theorem lemA: :: FIELD_12:9
for F being Field
for E being b1 -algebraic FieldExtension of F
for K being b2 -extending FieldExtension of F
for a being Element of K st a is E -algebraic holds
a is F -algebraic
proof end;

theorem e1a: :: FIELD_12:10
for F1, F2, L being Field
for E1 being FieldExtension of F1
for K1 being b4 -extending FieldExtension of F1
for h1 being Function of F1,L
for h2 being Function of E1,L
for h3 being Function of K1,L st h2 is h1 -extending & h3 is h2 -extending holds
h3 is h1 -extending
proof end;

registration
let F be Field;
cluster non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative F -extending -> F -homomorphic F -monomorphic for doubleLoopStr ;
coherence
for b1 being FieldExtension of F holds
( b1 is F -monomorphic & b1 is F -homomorphic )
proof end;
end;

registration
let F be Field;
let E be FieldExtension of F;
cluster non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible Abelian add-associative right_zeroed zeroed right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like gcd-like PID Euclidian F -homomorphic E -homomorphic K817() -homomorphic factorial F -monomorphic E -monomorphic for doubleLoopStr ;
existence
ex b1 being Field st
( b1 is E -homomorphic & b1 is E -monomorphic & b1 is F -homomorphic & b1 is F -monomorphic )
proof end;
end;

definition
mode sequence -> Function means :ds: :: FIELD_12:def 2
 dom it = NAT ;
existence
ex b1 being Function st dom b1 = NAT
proof end;
end;

:: deftheorem ds defines sequence FIELD_12:def 2 :
for b1 being Function holds
( b1 is sequence iff dom b1 = NAT );

registration
cluster -> NAT -defined for sequence ;
coherence
for b1 being sequence holds b1 is NAT -defined
proof end;
end;

definition
let f be Relation;
attr f is Field-yielding means :defFy: :: FIELD_12:def 3
 for x being object st x in rng f holds
x is Field;
end;

:: deftheorem defFy defines Field-yielding FIELD_12:def 3 :
for f being Relation holds
( f is Field-yielding iff for x being object st x in rng f holds
x is Field );

registration
cluster Relation-like NAT -defined Function-like Field-yielding for sequence ;
existence
ex b1 being sequence st b1 is Field-yielding
proof end;
end;

registration
cluster Relation-like Function-like Field-yielding -> 1-sorted-yielding for set ;
coherence
for b1 being Function st b1 is Field-yielding holds
b1 is 1-sorted-yielding
proof end;
end;

definition
let f be Field-yielding sequence ;
let i be Element of NAT ;
:: original: .
redefine func f . i -> Field;
coherence
f . i is Field
proof end;
end;

definition
let f be Field-yielding sequence ;
let i be Nat;
:: original: .
redefine func f . i -> Field;
coherence
f . i is Field
proof end;
end;

scheme :: FIELD_12:sch 1
RecExField{ F1() -> Field, P1[ object , Field, Field] } :
ex f being Field-yielding sequence st
( f . 0 = F1() & ( for n being Nat holds P1[n,f . n,f . (n + 1)] ) )
provided
A1: for n being Nat
for x being Field ex y being Field st P1[n,x,y]
proof end;

definition
let f be Field-yielding sequence ;
attr f is ascending means :defasc: :: FIELD_12:def 4
 for i being Element of NAT holds f . (i + 1) is FieldExtension of f . i;
end;

:: deftheorem defasc defines ascending FIELD_12:def 4 :
for f being Field-yielding sequence holds
( f is ascending iff for i being Element of NAT holds f . (i + 1) is FieldExtension of f . i );

registration
cluster Relation-like NAT -defined Function-like 1-sorted-yielding Field-yielding ascending for sequence ;
existence
ex b1 being Field-yielding sequence st b1 is ascending
proof end;
end;

definition
let f be Field-yielding sequence ;
func Carrier f -> non empty set equals :: FIELD_12:def 5
 union { the carrier of (f . i) where i is Element of NAT : verum } ;
coherence
union { the carrier of (f . i) where i is Element of NAT : verum } is non empty set
proof end;
end;

:: deftheorem defines Carrier FIELD_12:def 5 :
for f being Field-yielding sequence holds Carrier f = union { the carrier of (f . i) where i is Element of NAT : verum } ;

theorem lem1: :: FIELD_12:11
for f being Field-yielding ascending sequence
for i, j being Element of NAT
for a being Element of (f . i) st i <= j holds
a in the carrier of (f . j)
proof end;

theorem lem3: :: FIELD_12:12
for f being Field-yielding ascending sequence
for i, j being Element of NAT st i <= j holds
f . j is FieldExtension of f . i
proof end;

theorem lem2: :: FIELD_12:13
for f being Field-yielding ascending sequence
for i, j being Element of NAT
for xi, yi being Element of (f . i)
for xj, yj being Element of (f . j) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj )
proof end;

definition
let f be Field-yielding ascending sequence ;
func addseq f -> BinOp of (Carrier f) means :defadd: :: FIELD_12:def 6
 for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & it . (a,b) = x + y );
existence
ex b1 being BinOp of (Carrier f) st
for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & b1 . (a,b) = x + y )
proof end;
uniqueness
for b1, b2 being BinOp of (Carrier f) st ( for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & b1 . (a,b) = x + y ) ) & ( for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & b2 . (a,b) = x + y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defadd defines addseq FIELD_12:def 6 :
for f being Field-yielding ascending sequence
for b2 being BinOp of (Carrier f) holds
( b2 = addseq f iff for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & b2 . (a,b) = x + y ) );

definition
let f be Field-yielding ascending sequence ;
func multseq f -> BinOp of (Carrier f) means :defmult: :: FIELD_12:def 7
 for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & it . (a,b) = x * y );
existence
ex b1 being BinOp of (Carrier f) st
for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & b1 . (a,b) = x * y )
proof end;
uniqueness
for b1, b2 being BinOp of (Carrier f) st ( for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & b1 . (a,b) = x * y ) ) & ( for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & b2 . (a,b) = x * y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defmult defines multseq FIELD_12:def 7 :
for f being Field-yielding ascending sequence
for b2 being BinOp of (Carrier f) holds
( b2 = multseq f iff for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & b2 . (a,b) = x * y ) );

definition
let f be Field-yielding ascending sequence ;
func SeqField f -> strict doubleLoopStr means :dsf: :: FIELD_12:def 8
( the carrier of it = Carrier f & the addF of it = addseq f & the multF of it = multseq f & the OneF of it = 1. (f . 0) & the ZeroF of it = 0. (f . 0) );
existence
ex b1 being strict doubleLoopStr st
( the carrier of b1 = Carrier f & the addF of b1 = addseq f & the multF of b1 = multseq f & the OneF of b1 = 1. (f . 0) & the ZeroF of b1 = 0. (f . 0) )
proof end;
uniqueness
for b1, b2 being strict doubleLoopStr st the carrier of b1 = Carrier f & the addF of b1 = addseq f & the multF of b1 = multseq f & the OneF of b1 = 1. (f . 0) & the ZeroF of b1 = 0. (f . 0) & the carrier of b2 = Carrier f & the addF of b2 = addseq f & the multF of b2 = multseq f & the OneF of b2 = 1. (f . 0) & the ZeroF of b2 = 0. (f . 0) holds
b1 = b2 ;
end;

:: deftheorem dsf defines SeqField FIELD_12:def 8 :
for f being Field-yielding ascending sequence
for b2 being strict doubleLoopStr holds
( b2 = SeqField f iff ( the carrier of b2 = Carrier f & the addF of b2 = addseq f & the multF of b2 = multseq f & the OneF of b2 = 1. (f . 0) & the ZeroF of b2 = 0. (f . 0) ) );

theorem lem5: :: FIELD_12:14
for f being Field-yielding ascending sequence
for i being Element of NAT holds
( 1. (SeqField f) = 1. (f . i) & 0. (SeqField f) = 0. (f . i) )
proof end;

theorem lem4: :: FIELD_12:15
for f being Field-yielding ascending sequence
for a, b being Element of (SeqField f)
for i being Element of NAT
for x, y being Element of (f . i) st x = a & y = b holds
( a + b = x + y & a * b = x * y )
proof end;

registration
let f be Field-yielding ascending sequence ;
cluster SeqField f -> non degenerated strict ;
coherence
not SeqField f is degenerated
proof end;
end;

registration
let f be Field-yielding ascending sequence ;
cluster SeqField f -> right_complementable strict Abelian add-associative right_zeroed ;
coherence
( SeqField f is Abelian & SeqField f is add-associative & SeqField f is right_zeroed & SeqField f is right_complementable )
proof end;
end;

registration
let f be Field-yielding ascending sequence ;
cluster SeqField f -> almost_left_invertible strict well-unital distributive associative commutative ;
coherence
( SeqField f is commutative & SeqField f is associative & SeqField f is well-unital & SeqField f is distributive & SeqField f is almost_left_invertible )
proof end;
end;

theorem Fsub: :: FIELD_12:16
for f being Field-yielding ascending sequence
for i being Element of NAT holds f . i is Subfield of SeqField f
proof end;

theorem :: FIELD_12:17
for E being Field
for f being Field-yielding ascending sequence st ( for i being Element of NAT holds f . i is Subfield of E ) holds
SeqField f is Subfield of E
proof end;

theorem alg3a: :: FIELD_12:18
for f being Field-yielding ascending sequence
for X being finite Subset of (SeqField f) ex i being Element of NAT st X c= the carrier of (f . i)
proof end;

definition
let F be Field;
attr F is maximal_algebraic means :: FIELD_12:def 9
 for E being F -algebraic FieldExtension of F holds E == F;
end;

:: deftheorem defines maximal_algebraic FIELD_12:def 9 :
for F being Field holds
( F is maximal_algebraic iff for E being b1 -algebraic FieldExtension of F holds E == F );

al1: for F being Field holds
( F is algebraic-closed iff for p being irreducible Element of the carrier of (Polynom-Ring F) holds deg p = 1 )
proof end;

theorem eq: :: FIELD_12:19
for F being Field holds
( F is maximal_algebraic iff F is algebraic-closed )
proof end;

theorem alg2: :: FIELD_12:20
for F being Field holds
( F is algebraic-closed iff for p being non constant Polynomial of F holds p is with_roots )
proof end;

theorem :: FIELD_12:21
for F being Field holds
( F is algebraic-closed iff for p being irreducible Element of the carrier of (Polynom-Ring F) holds deg p = 1 ) by al1;

theorem :: FIELD_12:22
for F being Field holds
( F is algebraic-closed iff for p being non constant Polynomial of F holds p splits_in F )
proof end;

theorem :: FIELD_12:23
for F being Field holds
( F is algebraic-closed iff for p being non constant monic Polynomial of F holds p is Ppoly of F ) by RING_5:70;

theorem :: FIELD_12:24
for F being Field holds
( F is algebraic-closed iff for p, q being Element of the carrier of (Polynom-Ring F) holds
( p,q are_coprime iff p,q have_no_common_roots ) )
proof end;

theorem ClA: :: FIELD_12:25
for F being Field holds
( F is algebraic-closed iff for E being b1 -algebraic FieldExtension of F holds E == F )
proof end;

theorem :: FIELD_12:26
for F being Field holds
( F is algebraic-closed iff for E being b1 -finite FieldExtension of F holds E == F )
proof end;

registration
cluster non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative algebraic-closed -> infinite for doubleLoopStr ;
coherence
for b1 being Field st b1 is algebraic-closed holds
b1 is infinite ;
end;

definition
let F be Field;
mode ClosureSequence of F -> Field-yielding ascending sequence means :dA: :: FIELD_12:def 10
( it . 0 = F & ( for i being Element of NAT
for K being Field
for E being FieldExtension of K st K = it . i & E = it . (i + 1) holds
for p being non constant Element of the carrier of (Polynom-Ring K) holds p is_with_roots_in E ) );
existence
ex b1 being Field-yielding ascending sequence st
( b1 . 0 = F & ( for i being Element of NAT
for K being Field
for E being FieldExtension of K st K = b1 . i & E = b1 . (i + 1) holds
for p being non constant Element of the carrier of (Polynom-Ring K) holds p is_with_roots_in E ) )
proof end;
end;

:: deftheorem dA defines ClosureSequence FIELD_12:def 10 :
for F being Field
for b2 being Field-yielding ascending sequence holds
( b2 is ClosureSequence of F iff ( b2 . 0 = F & ( for i being Element of NAT
for K being Field
for E being FieldExtension of K st K = b2 . i & E = b2 . (i + 1) holds
for p being non constant Element of the carrier of (Polynom-Ring K) holds p is_with_roots_in E ) ) );

theorem alg3: :: FIELD_12:27
for f being Field-yielding ascending sequence
for p being Polynomial of (SeqField f) ex i being Element of NAT st p is Polynomial of (f . i)
proof end;

f12: for f being Field-yielding ascending sequence
for p being non constant Polynomial of (SeqField f) ex i being Element of NAT st p is non constant Polynomial of (f . i)
proof end;

registration
let F be Field;
let f be ClosureSequence of F;
cluster SeqField f -> strict F -extending ;
coherence
SeqField f is F -extending
proof end;
cluster SeqField f -> strict algebraic-closed ;
coherence
SeqField f is algebraic-closed
proof end;
end;

theorem main1: :: FIELD_12:28
for F being Field ex E being FieldExtension of F st E is algebraic-closed
proof end;

definition
let F be Field;
mode AlgebraicClosure of F -> FieldExtension of F means :defAC: :: FIELD_12:def 11
( it is F -algebraic & it is algebraic-closed );
existence
ex b1 being FieldExtension of F st
( b1 is F -algebraic & b1 is algebraic-closed )
proof end;
end;

:: deftheorem defAC defines AlgebraicClosure FIELD_12:def 11 :
for F being Field
for b2 being FieldExtension of F holds
( b2 is AlgebraicClosure of F iff ( b2 is F -algebraic & b2 is algebraic-closed ) );

registration
let F be Field;
cluster -> algebraic-closed F -algebraic for AlgebraicClosure of F;
coherence
for b1 being AlgebraicClosure of F holds
( b1 is F -algebraic & b1 is algebraic-closed ) by defAC;
end;

registration
let F be Field;
cluster non empty non degenerated non trivial infinite left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible Abelian add-associative right_zeroed zeroed right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like gcd-like algebraic-closed PID Euclidian F -homomorphic K817() -homomorphic factorial F -monomorphic for doubleLoopStr ;
existence
ex b1 being algebraic-closed Field st
( b1 is F -homomorphic & b1 is F -monomorphic )
proof end;
end;

theorem :: FIELD_12:29
for F being Field ex E being Field st E is AlgebraicClosure of F
proof end;

theorem XX: :: FIELD_12:30
for F being Field
for E being b1 -algebraic FieldExtension of F ex A being AlgebraicClosure of F st E is Subfield of A
proof end;

registration
let F be Field;
let E be F -algebraic FieldExtension of F;
cluster non empty non degenerated non trivial infinite left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible Abelian add-associative right_zeroed zeroed right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like gcd-like algebraic-closed PID Euclidian F -homomorphic Polynom-Ring F -homomorphic factorial F -monomorphic F -extending E -extending F -algebraic for AlgebraicClosure of F;
existence
ex b1 being AlgebraicClosure of F st b1 is E -extending
proof end;
end;

theorem :: FIELD_12:31
for F being Field
for E being b1 -algebraic FieldExtension of F
for A being AlgebraicClosure of E holds A is AlgebraicClosure of F
proof end;

theorem :: FIELD_12:32
for F being Field
for E being FieldExtension of F
for A being AlgebraicClosure of F st A is E -extending holds
A is AlgebraicClosure of E
proof end;

theorem lift3a: :: FIELD_12:33
for F being Field
for A1, A2 being AlgebraicClosure of F st A1 is A2 -extending holds
A2 == A1
proof end;

registration
let R be Ring;
let S be R -homomorphic Ring;
cluster non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed zeroed right-distributive left-distributive right_unital well-unital distributive left_unital unital associative R -homomorphic S -homomorphic K817() -homomorphic K817() -homomorphic for doubleLoopStr ;
existence
ex b1 being Ring st
( b1 is S -homomorphic & b1 is R -homomorphic )
proof end;
end;

registration
let R be Ring;
let S be R -homomorphic Ring;
let T be S -homomorphic Ring;
let f be additive Function of R,S;
let g be additive Function of S,T;
cluster f * g -> additive for Function of R,T;
coherence
for b1 being Function of R,T st b1 = g * f holds
b1 is additive
proof end;
end;

registration
let R be Ring;
let S be R -homomorphic Ring;
let T be S -homomorphic Ring;
let f be multiplicative Function of R,S;
let g be multiplicative Function of S,T;
cluster f * g -> multiplicative for Function of R,T;
coherence
for b1 being Function of R,T st b1 = g * f holds
b1 is multiplicative
proof end;
end;

registration
let R be Ring;
let S be R -homomorphic Ring;
let T be S -homomorphic Ring;
let f be unity-preserving Function of R,S;
let g be unity-preserving Function of S,T;
cluster f * g -> unity-preserving for Function of R,T;
coherence
for b1 being Function of R,T st b1 = g * f holds
b1 is unity-preserving ;
end;

theorem lift5a: :: FIELD_12:34
for F being Field
for E being FieldExtension of F holds id F is Monomorphism of F,E
proof end;

theorem ll: :: FIELD_12:35
for R being Ring
for S being b1 -homomorphic Ring
for T being b1 -homomorphic b2 -homomorphic Ring
for f being additive Function of R,S
for g being additive Function of S,T holds PolyHom (g * f) = (PolyHom g) * (PolyHom f)
proof end;

ll2: for R being Ring
for S being b1 -homomorphic Ring
for T being b1 -homomorphic b2 -homomorphic Ring
for f being additive Function of R,S
for g being additive Function of S,T st g * f = id R holds
(PolyHom g) * (PolyHom f) = id (Polynom-Ring R)
proof end;

theorem :: FIELD_12:36
for R being Ring
for S being b1 -homomorphic Ring
for T being b1 -homomorphic b2 -homomorphic Ring
for f being additive Function of R,S
for g being additive Function of S,T st g * f = id R holds
PolyHom (g * f) = id (Polynom-Ring R)
proof end;

theorem lift9: :: FIELD_12:37
for F1, F2 being Field
for E being FieldExtension of F1 st F1 == F2 holds
E is FieldExtension of F2
proof end;

theorem lift6b: :: FIELD_12:38
for F1, F2 being Field st F1 == F2 holds
( 0_. F1 = 0_. F2 & 1_. F1 = 1_. F2 )
proof end;

theorem lift6a: :: FIELD_12:39
for F1, F2 being Field
for p being Polynomial of F1 st F1 == F2 holds
p is Polynomial of F2
proof end;

theorem lift6: :: FIELD_12:40
for F1, F2 being Field
for p being non zero Polynomial of F1 st F1 == F2 holds
p is non zero Polynomial of F2
proof end;

theorem lift8: :: FIELD_12:41
for F1, F2 being Field
for p being Polynomial of F1
for q being Polynomial of F2
for a being Element of F1
for b being Element of F2 st F1 == F2 & p = q & a = b holds
eval (p,a) = eval (q,b)
proof end;

theorem lift7: :: FIELD_12:42
for F1, F2 being Field
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for p being Polynomial of F1
for q being Polynomial of F2
for a being Element of E1
for b being Element of E2 st F1 == F2 & E1 == E2 & p = q & a = b holds
Ext_eval (p,a) = Ext_eval (q,b)
proof end;

theorem lift5: :: FIELD_12:43
for F1, F2 being Field
for E being b1 -algebraic FieldExtension of F1 st F1 == F2 holds
E is b2 -algebraic FieldExtension of F2
proof end;

theorem lift4: :: FIELD_12:44
for F1, F2 being Field
for E being AlgebraicClosure of F1 st F1 == F2 holds
E is AlgebraicClosure of F2
proof end;

definition
let X be set ;
attr X is Field-membered means :defFm: :: FIELD_12:def 12
 for x being object st x in X holds
x is Field;
end;

:: deftheorem defFm defines Field-membered FIELD_12:def 12 :
for X being set holds
( X is Field-membered iff for x being object st x in X holds
x is Field );

registration
cluster non empty Field-membered for set ;
existence
ex b1 being set st
( b1 is Field-membered & not b1 is empty )
proof end;
end;

definition
let X be non empty Field-membered set ;
:: original: Element
redefine mode Element of X -> Field;
coherence
for b1 being Element of X holds b1 is Field by defFm;
end;

definition
let F be Field;
func SubFields F -> set means :defX: :: FIELD_12:def 13
 for o being object holds
( o in it iff ex K being strict Field st
( o = K & K is Subfield of F ) );
existence
ex b1 being set st
for o being object holds
( o in b1 iff ex K being strict Field st
( o = K & K is Subfield of F ) )
proof end;
uniqueness
for b1, b2 being set st ( for o being object holds
( o in b1 iff ex K being strict Field st
( o = K & K is Subfield of F ) ) ) & ( for o being object holds
( o in b2 iff ex K being strict Field st
( o = K & K is Subfield of F ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defX defines SubFields FIELD_12:def 13 :
for F being Field
for b2 being set holds
( b2 = SubFields F iff for o being object holds
( o in b2 iff ex K being strict Field st
( o = K & K is Subfield of F ) ) );

registration
let F be Field;
cluster SubFields F -> non empty Field-membered ;
coherence
( not SubFields F is empty & SubFields F is Field-membered )
proof end;
end;

theorem subfie: :: FIELD_12:45
for F, K being Field holds
( K in SubFields F iff K is strict Subfield of F )
proof end;

definition
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
func Ext_Set (f,E) -> non empty set equals :: FIELD_12:def 14
 { [K,g] where K is Element of SubFields E, g is Function of K,L : ex K1 being FieldExtension of F ex g1 being Function of K1,L st
( K1 = K & g1 = g & g1 is monomorphism & g1 is f -extending ) } ;
coherence
{ [K,g] where K is Element of SubFields E, g is Function of K,L : ex K1 being FieldExtension of F ex g1 being Function of K1,L st
( K1 = K & g1 = g & g1 is monomorphism & g1 is f -extending ) } is non empty set
proof end;
end;

:: deftheorem defines Ext_Set FIELD_12:def 14 :
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L holds Ext_Set (f,E) = { [K,g] where K is Element of SubFields E, g is Function of K,L : ex K1 being FieldExtension of F ex g1 being Function of K1,L st
( K1 = K & g1 = g & g1 is monomorphism & g1 is f -extending ) } ;

registration
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
cluster -> pair for Element of Ext_Set (f,E);
coherence
for b1 being Element of Ext_Set (f,E) holds b1 is pair
proof end;
end;

definition
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
let p be Element of Ext_Set (f,E);
:: original: `1
redefine func p `1 -> strict FieldExtension of F;
coherence
p `1 is strict FieldExtension of F
proof end;
end;

definition
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
let p be Element of Ext_Set (f,E);
:: original: `2
redefine func p `2 -> Function of (p `1),L;
coherence
p `2 is Function of (p `1),L
proof end;
end;

theorem inS: :: FIELD_12:46
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for K being strict FieldExtension of F
for g being Function of K,L st g is monomorphism holds
( [K,g] in Ext_Set (f,E) iff ( E is FieldExtension of K & F is Subfield of K & g is f -extending ) )
proof end;

definition
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
let p, q be Element of Ext_Set (f,E);
pred p <= q means :: FIELD_12:def 15
( q `1 is FieldExtension of p `1 & ( for K being FieldExtension of p `1
for g being Function of K,L st K = q `1 & g = q `2 holds
g is p `2 -extending ) );
end;

:: deftheorem defines <= FIELD_12:def 15 :
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for p, q being Element of Ext_Set (f,E) holds
( p <= q iff ( q `1 is FieldExtension of p `1 & ( for K being FieldExtension of p `1
for g being Function of K,L st K = q `1 & g = q `2 holds
g is p `2 -extending ) ) );

definition
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
let S be non empty Subset of (Ext_Set (f,E));
attr S is ascending means :dasc: :: FIELD_12:def 16
 for p, q being Element of S holds
( p <= q or q <= p );
end;

:: deftheorem dasc defines ascending FIELD_12:def 16 :
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty Subset of (Ext_Set (f,E)) holds
( S is ascending iff for p, q being Element of S holds
( p <= q or q <= p ) );

registration
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
cluster non empty ascending for Element of bool (Ext_Set (f,E));
existence
ex b1 being non empty Subset of (Ext_Set (f,E)) st b1 is ascending
proof end;
end;

theorem po1: :: FIELD_12:47
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for p being Element of Ext_Set (f,E) holds p <= p
proof end;

theorem po2: :: FIELD_12:48
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for p, q being Element of Ext_Set (f,E) st p <= q & q <= p holds
p = q
proof end;

theorem po3: :: FIELD_12:49
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for p, q, r being Element of Ext_Set (f,E) st p <= q & q <= r holds
p <= r
proof end;

definition
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
let S be non empty Subset of (Ext_Set (f,E));
func unionCarrier (S,f,E) -> non empty set equals :: FIELD_12:def 17
 union { the carrier of (p `1) where p is Element of S : verum } ;
coherence
union { the carrier of (p `1) where p is Element of S : verum } is non empty set
proof end;
end;

:: deftheorem defines unionCarrier FIELD_12:def 17 :
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty Subset of (Ext_Set (f,E)) holds unionCarrier (S,f,E) = union { the carrier of (p `1) where p is Element of S : verum } ;

definition
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
let S be non empty ascending Subset of (Ext_Set (f,E));
func unionAdd (S,f,E) -> BinOp of (unionCarrier (S,f,E)) means :dua: :: FIELD_12:def 18
 for a, b being Element of unionCarrier (S,f,E) ex p being Element of S ex x, y being Element of (p `1) st
( x = a & y = b & it . (a,b) = x + y );
existence
ex b1 being BinOp of (unionCarrier (S,f,E)) st
for a, b being Element of unionCarrier (S,f,E) ex p being Element of S ex x, y being Element of (p `1) st
( x = a & y = b & b1 . (a,b) = x + y )
proof end;
uniqueness
for b1, b2 being BinOp of (unionCarrier (S,f,E)) st ( for a, b being Element of unionCarrier (S,f,E) ex p being Element of S ex x, y being Element of (p `1) st
( x = a & y = b & b1 . (a,b) = x + y ) ) & ( for a, b being Element of unionCarrier (S,f,E) ex p being Element of S ex x, y being Element of (p `1) st
( x = a & y = b & b2 . (a,b) = x + y ) ) holds
b1 = b2
proof end;
func unionMult (S,f,E) -> BinOp of (unionCarrier (S,f,E)) means :dum: :: FIELD_12:def 19
 for a, b being Element of unionCarrier (S,f,E) ex p being Element of S ex x, y being Element of (p `1) st
( x = a & y = b & it . (a,b) = x * y );
existence
ex b1 being BinOp of (unionCarrier (S,f,E)) st
for a, b being Element of unionCarrier (S,f,E) ex p being Element of S ex x, y being Element of (p `1) st
( x = a & y = b & b1 . (a,b) = x * y )
proof end;
uniqueness
for b1, b2 being BinOp of (unionCarrier (S,f,E)) st ( for a, b being Element of unionCarrier (S,f,E) ex p being Element of S ex x, y being Element of (p `1) st
( x = a & y = b & b1 . (a,b) = x * y ) ) & ( for a, b being Element of unionCarrier (S,f,E) ex p being Element of S ex x, y being Element of (p `1) st
( x = a & y = b & b2 . (a,b) = x * y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem dua defines unionAdd FIELD_12:def 18 :
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for b6 being BinOp of (unionCarrier (S,f,E)) holds
( b6 = unionAdd (S,f,E) iff for a, b being Element of unionCarrier (S,f,E) ex p being Element of S ex x, y being Element of (p `1) st
( x = a & y = b & b6 . (a,b) = x + y ) );

:: deftheorem dum defines unionMult FIELD_12:def 19 :
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for b6 being BinOp of (unionCarrier (S,f,E)) holds
( b6 = unionMult (S,f,E) iff for a, b being Element of unionCarrier (S,f,E) ex p being Element of S ex x, y being Element of (p `1) st
( x = a & y = b & b6 . (a,b) = x * y ) );

definition
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
let S be non empty ascending Subset of (Ext_Set (f,E));
func unionOne (S,f,E) -> Element of unionCarrier (S,f,E) means :defone: :: FIELD_12:def 20
 ex p being Element of S st it = 1. (p `1);
existence
ex b1 being Element of unionCarrier (S,f,E) ex p being Element of S st b1 = 1. (p `1)
proof end;
uniqueness
for b1, b2 being Element of unionCarrier (S,f,E) st ex p being Element of S st b1 = 1. (p `1) & ex p being Element of S st b2 = 1. (p `1) holds
b1 = b2
proof end;
func unionZero (S,f,E) -> Element of unionCarrier (S,f,E) means :defzero: :: FIELD_12:def 21
 ex p being Element of S st it = 0. (p `1);
existence
ex b1 being Element of unionCarrier (S,f,E) ex p being Element of S st b1 = 0. (p `1)
proof end;
uniqueness
for b1, b2 being Element of unionCarrier (S,f,E) st ex p being Element of S st b1 = 0. (p `1) & ex p being Element of S st b2 = 0. (p `1) holds
b1 = b2
proof end;
end;

:: deftheorem defone defines unionOne FIELD_12:def 20 :
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for b6 being Element of unionCarrier (S,f,E) holds
( b6 = unionOne (S,f,E) iff ex p being Element of S st b6 = 1. (p `1) );

:: deftheorem defzero defines unionZero FIELD_12:def 21 :
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for b6 being Element of unionCarrier (S,f,E) holds
( b6 = unionZero (S,f,E) iff ex p being Element of S st b6 = 0. (p `1) );

definition
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
let S be non empty ascending Subset of (Ext_Set (f,E));
func unionField (S,f,E) -> strict doubleLoopStr means :duf: :: FIELD_12:def 22
( the carrier of it = unionCarrier (S,f,E) & the addF of it = unionAdd (S,f,E) & the multF of it = unionMult (S,f,E) & the OneF of it = unionOne (S,f,E) & the ZeroF of it = unionZero (S,f,E) );
existence
ex b1 being strict doubleLoopStr st
( the carrier of b1 = unionCarrier (S,f,E) & the addF of b1 = unionAdd (S,f,E) & the multF of b1 = unionMult (S,f,E) & the OneF of b1 = unionOne (S,f,E) & the ZeroF of b1 = unionZero (S,f,E) )
proof end;
uniqueness
for b1, b2 being strict doubleLoopStr st the carrier of b1 = unionCarrier (S,f,E) & the addF of b1 = unionAdd (S,f,E) & the multF of b1 = unionMult (S,f,E) & the OneF of b1 = unionOne (S,f,E) & the ZeroF of b1 = unionZero (S,f,E) & the carrier of b2 = unionCarrier (S,f,E) & the addF of b2 = unionAdd (S,f,E) & the multF of b2 = unionMult (S,f,E) & the OneF of b2 = unionOne (S,f,E) & the ZeroF of b2 = unionZero (S,f,E) holds
b1 = b2 ;
end;

:: deftheorem duf defines unionField FIELD_12:def 22 :
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for b6 being strict doubleLoopStr holds
( b6 = unionField (S,f,E) iff ( the carrier of b6 = unionCarrier (S,f,E) & the addF of b6 = unionAdd (S,f,E) & the multF of b6 = unionMult (S,f,E) & the OneF of b6 = unionOne (S,f,E) & the ZeroF of b6 = unionZero (S,f,E) ) );

theorem lem1a: :: FIELD_12:50
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty Subset of (Ext_Set (f,E))
for p, q being Element of S
for a being Element of (p `1) st p <= q holds
a in the carrier of (q `1)
proof end;

theorem lem5a: :: FIELD_12:51
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for p being Element of S holds
( 1. (unionField (S,f,E)) = 1. (p `1) & 0. (unionField (S,f,E)) = 0. (p `1) )
proof end;

theorem lem4a: :: FIELD_12:52
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for a, b being Element of (unionField (S,f,E))
for p being Element of S
for x, y being Element of (p `1) st x = a & y = b holds
( a + b = x + y & a * b = x * y )
proof end;

registration
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
let S be non empty ascending Subset of (Ext_Set (f,E));
cluster unionField (S,f,E) -> non degenerated strict ;
coherence
not unionField (S,f,E) is degenerated
proof end;
end;

registration
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
let S be non empty ascending Subset of (Ext_Set (f,E));
cluster unionField (S,f,E) -> right_complementable strict Abelian add-associative right_zeroed ;
coherence
( unionField (S,f,E) is Abelian & unionField (S,f,E) is add-associative & unionField (S,f,E) is right_zeroed & unionField (S,f,E) is right_complementable )
proof end;
end;

registration
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
let S be non empty ascending Subset of (Ext_Set (f,E));
cluster unionField (S,f,E) -> almost_left_invertible strict well-unital distributive associative commutative ;
coherence
( unionField (S,f,E) is commutative & unionField (S,f,E) is associative & unionField (S,f,E) is well-unital & unionField (S,f,E) is distributive & unionField (S,f,E) is almost_left_invertible )
proof end;
end;

theorem Fsubb: :: FIELD_12:53
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for p being Element of S holds p `1 is Subfield of unionField (S,f,E)
proof end;

theorem Fsuba: :: FIELD_12:54
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E)) holds F is Subfield of unionField (S,f,E)
proof end;

theorem inSa: :: FIELD_12:55
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E)) holds unionField (S,f,E) is Subfield of E
proof end;

registration
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
let S be non empty ascending Subset of (Ext_Set (f,E));
cluster unionField (S,f,E) -> strict F -extending ;
coherence
unionField (S,f,E) is F -extending
proof end;
end;

definition
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
let S be non empty ascending Subset of (Ext_Set (f,E));
func unionExt (S,f,E) -> Function of (unionField (S,f,E)),L means :dufe: :: FIELD_12:def 23
 for p being Element of S holds it | the carrier of (p `1) = p `2 ;
existence
ex b1 being Function of (unionField (S,f,E)),L st
for p being Element of S holds b1 | the carrier of (p `1) = p `2
proof end;
uniqueness
for b1, b2 being Function of (unionField (S,f,E)),L st ( for p being Element of S holds b1 | the carrier of (p `1) = p `2 ) & ( for p being Element of S holds b2 | the carrier of (p `1) = p `2 ) holds
b1 = b2
proof end;
end;

:: deftheorem dufe defines unionExt FIELD_12:def 23 :
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for b6 being Function of (unionField (S,f,E)),L holds
( b6 = unionExt (S,f,E) iff for p being Element of S holds b6 | the carrier of (p `1) = p `2 );

theorem inSb: :: FIELD_12:56
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E)) holds
( unionExt (S,f,E) is monomorphism & unionExt (S,f,E) is f -extending )
proof end;

definition
let F be Field;
let E be FieldExtension of F;
let L be F -monomorphic Field;
let f be Monomorphism of F,L;
let S be non empty ascending Subset of (Ext_Set (f,E));
func upper_bound S -> Element of Ext_Set (f,E) equals :: FIELD_12:def 24
[(unionField (S,f,E)),(unionExt (S,f,E))];
coherence
[(unionField (S,f,E)),(unionExt (S,f,E))] is Element of Ext_Set (f,E)
proof end;
end;

:: deftheorem defines upper_bound FIELD_12:def 24 :
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E)) holds upper_bound S = [(unionField (S,f,E)),(unionExt (S,f,E))];

theorem up: :: FIELD_12:57
for F being Field
for E being FieldExtension of F
for L being b1 -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for p being Element of S holds p <= upper_bound S
proof end;

theorem lift1: :: FIELD_12:58
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for L being algebraic-closed b1 -monomorphic Field
for f being Monomorphism of F,L ex g being Function of (FAdj (F,{a})),L st
( g is monomorphism & g is f -extending )
proof end;

theorem lift2: :: FIELD_12:59
for F being Field
for E being b1 -algebraic FieldExtension of F
for L being algebraic-closed b1 -monomorphic Field
for f being Monomorphism of F,L ex g being Function of E,L st
( g is monomorphism & g is f -extending )
proof end;

theorem lift3b: :: FIELD_12:60
for F being Field
for E being FieldExtension of F
for L being b1 -homomorphic b2 -homomorphic Field
for f being Homomorphism of F,L
for g being Homomorphism of E,L st g is f -extending holds
Image f is Subfield of Image g
proof end;

theorem lift3c: :: FIELD_12:61
for F being Field
for A being AlgebraicClosure of F
for L being b2 -homomorphic b2 -monomorphic Field
for g being Monomorphism of A,L holds Image g is algebraic-closed
proof end;

theorem lift3: :: FIELD_12:62
for F being Field
for L being b1 -homomorphic b1 -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
proof end;

theorem :: FIELD_12:63
for F being Field
for A1, A2 being AlgebraicClosure of F holds A1,A2 are_isomorphic_over F
proof end;