let F be Field; :: thesis: for E being FieldExtension of F
for L being F -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 )
let E be FieldExtension of F; :: thesis: for L being F -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 )
let L be F -monomorphic Field; :: thesis: 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 )
let f be Monomorphism of F,L; :: thesis: 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 )
let S be non empty ascending Subset of (Ext_Set (f,E)); :: thesis: ( unionExt (S,f,E) is monomorphism & unionExt (S,f,E) is f -extending )
set K = unionField (S,f,E);
set h = unionExt (S,f,E);
set p = the Element of S;
H: the carrier of (unionField (S,f,E)) = unionCarrier (S,f,E) by duf;
the Element of S in Ext_Set (f,E) ;
then consider U being Element of SubFields E, g being Function of U,L such that
A3: ( the Element of S = [U,g] & ex K1 being FieldExtension of F ex g1 being Function of K1,L st
( K1 = U & g1 = g & g1 is monomorphism & g1 is f -extending ) ) ;
consider K1 being FieldExtension of F, g1 being Function of K1,L such that
A4: ( K1 = U & g1 = g & g1 is monomorphism & g1 is f -extending ) by A3;
AS3: the Element of S `1 = U by A3;
AS4: the Element of S `2 = g by A3;
D: 1. (unionField (S,f,E)) = 1. K1 by A4, AS3, lem5a;
F: (unionExt (S,f,E)) | the carrier of K1 = g by A4, AS4, dufe;
E: ( g is additive & g is multiplicative & g is unity-preserving ) by A4;

A: now :: thesis: for a, b being Element of (unionField (S,f,E)) holds ((unionExt (S,f,E)) . a) + ((unionExt (S,f,E)) . b) = (unionExt (S,f,E)) . (a + b)

let a, b be Element of (unionField (S,f,E)); :: thesis: ((unionExt (S,f,E)) . a) + ((unionExt (S,f,E)) . b) = (unionExt (S,f,E)) . (a + b)
consider p being Element of S, x, y being Element of (p `1) such that
A1: ( x = a & y = b & (unionAdd (S,f,E)) . (a,b) = x + y ) by H, dua;
A2: (unionExt (S,f,E)) | the carrier of (p `1) = p `2 by dufe;
then A3: ( (unionExt (S,f,E)) . a = (p `2) . x & (unionExt (S,f,E)) . b = (p `2) . y ) by A1, FUNCT_1:49;
p in Ext_Set (f,E) ;
then consider U being Element of SubFields E, g2 being Function of U,L such that
A7: ( p = [U,g2] & ex K1 being FieldExtension of F ex g1 being Function of K1,L st
( K1 = U & g1 = g2 & g1 is monomorphism & g1 is f -extending ) ) ;
A4: p `2 is additive by A7;
A5: x + y = a + b by A1, duf;
thus ((unionExt (S,f,E)) . a) + ((unionExt (S,f,E)) . b) = (p `2) . (x + y) by A4, A3
.= (unionExt (S,f,E)) . (a + b) by A2, A5, FUNCT_1:49 ; :: thesis: verum

end;

B: now :: thesis: for a, b being Element of (unionField (S,f,E)) holds ((unionExt (S,f,E)) . a) * ((unionExt (S,f,E)) . b) = (unionExt (S,f,E)) . (a * b)

let a, b be Element of (unionField (S,f,E)); :: thesis: ((unionExt (S,f,E)) . a) * ((unionExt (S,f,E)) . b) = (unionExt (S,f,E)) . (a * b)
consider p being Element of S, x, y being Element of (p `1) such that
A1: ( x = a & y = b & (unionMult (S,f,E)) . (a,b) = x * y ) by H, dum;
A2: (unionExt (S,f,E)) | the carrier of (p `1) = p `2 by dufe;
then A3: ( (unionExt (S,f,E)) . a = (p `2) . x & (unionExt (S,f,E)) . b = (p `2) . y ) by A1, FUNCT_1:49;
p in Ext_Set (f,E) ;
then consider U being Element of SubFields E, g2 being Function of U,L such that
A7: ( p = [U,g2] & ex K1 being FieldExtension of F ex g1 being Function of K1,L st
( K1 = U & g1 = g2 & g1 is monomorphism & g1 is f -extending ) ) ;
A4: p `2 is multiplicative by A7;
A5: x * y = a * b by A1, duf;
thus ((unionExt (S,f,E)) . a) * ((unionExt (S,f,E)) . b) = (p `2) . (x * y) by A4, A3
.= (unionExt (S,f,E)) . (a * b) by A2, A5, FUNCT_1:49 ; :: thesis: verum

end;

( unionExt (S,f,E) is additive & unionExt (S,f,E) is multiplicative & unionExt (S,f,E) is unity-preserving ) by A, B, E, A4, D, F, FUNCT_1:49;
hence unionExt (S,f,E) is monomorphism ; :: thesis: unionExt (S,f,E) is f -extending
set p = the Element of S;
the Element of S in Ext_Set (f,E) ;
then consider U being Element of SubFields E, g being Function of U,L such that
A3: ( the Element of S = [U,g] & ex K1 being FieldExtension of F ex g1 being Function of K1,L st
( K1 = U & g1 = g & g1 is monomorphism & g1 is f -extending ) ) ;
consider K1 being FieldExtension of F, g1 being Function of K1,L such that
A4: ( K1 = U & g1 = g & g1 is monomorphism & g1 is f -extending ) by A3;
reconsider L1 = L as FieldExtension of L by FIELD_4:6;
the Element of S `1 is Subfield of unionField (S,f,E) by Fsubb;
then reconsider K = unionField (S,f,E) as K1 -extending FieldExtension of F by A3, A4, FIELD_4:7;
reconsider h = unionExt (S,f,E) as Function of K,L1 ;
A7: the Element of S `2 = g1 by A3, A4;

now :: thesis: for a being Element of K1 holds g1 . a = h . a

let a be Element of K1; :: thesis: g1 . a = h . a
h | the carrier of K1 = g1 by A7, dufe;
hence g1 . a = h . a by FUNCT_1:49; :: thesis: verum

end;

then h is g1 -extending ;
hence unionExt (S,f,E) is f -extending by A4, FIELD_8:41; :: thesis: verum