let F be 0 -characteristic Field; :: thesis:
let E be FieldExtension of F; :: thesis:
let a, b be F -algebraic Element of E; :: thesis:
set K = FAdj (F,{a,b});
set ma = MinPoly (a,F);
set mb = MinPoly (b,F);
( {a,b} is Subset of (FAdj (F,{a,b})) & a in {a,b} & b in {a,b} ) by FIELD_6:35, TARSKI:def 2;
then reconsider aK = a, bK = b as Element of (FAdj (F,{a,b})) ;
consider Z being FieldExtension of E such that
V: Z is algebraic-closed by FIELD_12:28;
S: E is Subfield of Z by FIELD_4:7;
then U: FAdj (F,{a,b}) is Subfield of Z by EC_PF_1:5;
then reconsider Z = Z as FAdj (F,{a,b}) -extending FieldExtension of F by FIELD_4:7;
set Rma = Roots (Z,(MinPoly (a,F)));
set Rmb = (Roots (Z,(MinPoly (b,F)))) \ {b};
ex x being Element of F st
for c, d being Element of Z st c in Roots (Z,(MinPoly (a,F))) & d in (Roots (Z,(MinPoly (b,F)))) \ {b} holds
(@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z))) <> c + ((@ (x,Z)) * d)

suppose W: ( Roots (Z,(MinPoly (a,F))) = {} or (Roots (Z,(MinPoly (b,F)))) \ {b} = {} ) ; :: thesis:

take 1. F ; :: thesis:
thus for c, d being Element of Z st c in Roots (Z,(MinPoly (a,F))) & d in (Roots (Z,(MinPoly (b,F)))) \ {b} holds
(@ (aK,Z)) + ((@ ((1. F),Z)) * (@ (bK,Z))) <> c + ((@ ((1. F),Z)) * d) by W; :: thesis:

end;

suppose W: ( Roots (Z,(MinPoly (a,F))) <> {} & (Roots (Z,(MinPoly (b,F)))) \ {b} <> {} ) ; :: thesis:

set M = { ((c - (@ (aK,Z))) * (((@ (bK,Z)) - d) ")) where c, d is Element of Z : ( c in Roots (Z,(MinPoly (a,F))) & d in (Roots (Z,(MinPoly (b,F)))) \ {b} ) } ;
{ ((c - (@ (aK,Z))) * (((@ (bK,Z)) - d) ")) where c, d is Element of Z : ( c in Roots (Z,(MinPoly (a,F))) & d in (Roots (Z,(MinPoly (b,F)))) \ {b} ) } <> {}

proof

set c = the Element of Roots (Z,(MinPoly (a,F)));
set d = the Element of (Roots (Z,(MinPoly (b,F)))) \ {b};
( the Element of Roots (Z,(MinPoly (a,F))) in Roots (Z,(MinPoly (a,F))) & the Element of (Roots (Z,(MinPoly (b,F)))) \ {b} in (Roots (Z,(MinPoly (b,F)))) \ {b} ) by W;
then reconsider c = the Element of Roots (Z,(MinPoly (a,F))), d = the Element of (Roots (Z,(MinPoly (b,F)))) \ {b} as Element of Z ;
(c - (@ (aK,Z))) * (((@ (bK,Z)) - d) ") in { ((c - (@ (aK,Z))) * (((@ (bK,Z)) - d) ")) where c, d is Element of Z : ( c in Roots (Z,(MinPoly (a,F))) & d in (Roots (Z,(MinPoly (b,F)))) \ {b} ) } by W;
hence { ((c - (@ (aK,Z))) * (((@ (bK,Z)) - d) ")) where c, d is Element of Z : ( c in Roots (Z,(MinPoly (a,F))) & d in (Roots (Z,(MinPoly (b,F)))) \ {b} ) } <> {} ; :: thesis:

end;

then reconsider M = { ((c - (@ (aK,Z))) * (((@ (bK,Z)) - d) ")) where c, d is Element of Z : ( c in Roots (Z,(MinPoly (a,F))) & d in (Roots (Z,(MinPoly (b,F)))) \ {b} ) } as non empty set ;
F: M is finite

proof

defpred S₁[ object , object ] means ex c, d being Element of Z st
( c in Roots (Z,(MinPoly (a,F))) & d in (Roots (Z,(MinPoly (b,F)))) \ {b} & $1 = [c,d] & $2 = (c - (@ (aK,Z))) * (((@ (bK,Z)) - d) ") );

F1: now :: thesis:

let x be object ; :: thesis:
assume x in [:(Roots (Z,(MinPoly (a,F)))),((Roots (Z,(MinPoly (b,F)))) \ {b}):] ; :: thesis:
then consider c, d being object such that
F2: ( c in Roots (Z,(MinPoly (a,F))) & d in (Roots (Z,(MinPoly (b,F)))) \ {b} & x = [c,d] ) by ZFMISC_1:def 2;
reconsider c = c, d = d as Element of Z by F2;
(c - (@ (aK,Z))) * (((@ (bK,Z)) - d) ") in M by F2;
hence ex y being object st
( y in M & S₁[x,y] ) by F2; :: thesis:

end;

consider f being Function of [:(Roots (Z,(MinPoly (a,F)))),((Roots (Z,(MinPoly (b,F)))) \ {b}):],M such that
F2: for x being object st x in [:(Roots (Z,(MinPoly (a,F)))),((Roots (Z,(MinPoly (b,F)))) \ {b}):] holds
S₁[x,f . x] from FUNCT_2:sch 1(F1);
M c= rng f

proof

now :: thesis:

let o be object ; :: thesis:
assume o in M ; :: thesis:
then consider c, d being Element of Z such that
F5: ( o = (c - (@ (aK,Z))) * (((@ (bK,Z)) - d) ") & c in Roots (Z,(MinPoly (a,F))) & d in (Roots (Z,(MinPoly (b,F)))) \ {b} ) ;
F6: [c,d] in [:(Roots (Z,(MinPoly (a,F)))),((Roots (Z,(MinPoly (b,F)))) \ {b}):] by F5, ZFMISC_1:def 2;
then F7: [c,d] in dom f by FUNCT_2:def 1;
S₁[[c,d],f . [c,d]] by F6, F2;
then consider c1, d1 being Element of Z such that
F8: ( [c1,d1] = [c,d] & f . [c1,d1] = (c1 - (@ (aK,Z))) * (((@ (bK,Z)) - d1) ") ) ;
( c1 = c & d1 = d ) by F8, XTUPLE_0:1;
hence o in rng f by F8, F5, F7, FUNCT_1:def 3; :: thesis:

end;

hence M c= rng f ; :: thesis:

end;

hence M is finite ; :: thesis:

end;

now :: thesis:

assume G: for x being Element of F ex c, d being Element of Z st
( c in Roots (Z,(MinPoly (a,F))) & d in (Roots (Z,(MinPoly (b,F)))) \ {b} & (@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z))) = c + ((@ (x,Z)) * d) ) ; :: thesis:

now :: thesis:

let o be object ; :: thesis:
assume o in the carrier of F ; :: thesis:
then reconsider x = o as Element of F ;
consider c, d being Element of Z such that
G1: ( c in Roots (Z,(MinPoly (a,F))) & d in (Roots (Z,(MinPoly (b,F)))) \ {b} & (@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z))) = c + ((@ (x,Z)) * d) ) by G;

G3: now :: thesis:

assume (@ (bK,Z)) - d = 0. Z ; :: thesis:
then @ (bK,Z) = (0. Z) + d by VECTSP_2:2;
then d = b by FIELD_7:def 4;
then not b in {b} by G1, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis:

end;

(@ (x,Z)) * (@ (bK,Z)) = (c + ((@ (x,Z)) * d)) - (@ (aK,Z)) by G1, VECTSP_2:2
.= (c + (- (@ (aK,Z)))) + ((@ (x,Z)) * d) by RLVECT_1:def 3 ;
then c - (@ (aK,Z)) = ((@ (x,Z)) * (@ (bK,Z))) - ((@ (x,Z)) * d) by VECTSP_2:2
.= (@ (x,Z)) * ((@ (bK,Z)) - d) by VECTSP_1:11 ;
then (c - (@ (aK,Z))) * (((@ (bK,Z)) - d) ") = (@ (x,Z)) * (((@ (bK,Z)) - d) * (((@ (bK,Z)) - d) ")) by GROUP_1:def 3
.= (@ (x,Z)) * (1. Z) by G3, VECTSP_2:def 2
.= x by FIELD_7:def 4 ;
hence o in M by G1; :: thesis:

end;

then the carrier of F c= M ;
hence F is finite by F; :: thesis:

end;

hence ex x being Element of F st
for c, d being Element of Z st c in Roots (Z,(MinPoly (a,F))) & d in (Roots (Z,(MinPoly (b,F)))) \ {b} holds
(@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z))) <> c + ((@ (x,Z)) * d) ; :: thesis:

end;

then consider x being Element of F such that
A: for c, d being Element of Z st c in Roots (Z,(MinPoly (a,F))) & d in (Roots (Z,(MinPoly (b,F)))) \ {b} holds
(@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z))) <> c + ((@ (x,Z)) * d) ;
set lZ = (@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z)));
set G = FAdj (F,{((@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z))))});
reconsider G = FAdj (F,{((@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z))))}) as FieldExtension of F ;
B: G is Subfield of FAdj (F,{a,b})

proof

H: ( F is Subfield of FAdj (F,{a,b}) & F is Subfield of FAdj (F,{((@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z))))}) ) by FIELD_4:7;
then the carrier of F c= the carrier of (FAdj (F,{a,b})) by EC_PF_1:def 1;
then reconsider x1 = x as Element of (FAdj (F,{a,b})) ;
I: ( FAdj (F,{a,b}) is Subring of Z & @ (x,Z) = x & @ (bK,Z) = bK & @ (aK,Z) = aK ) by U, FIELD_5:12, FIELD_7:def 4;
then x1 * bK = (@ (x,Z)) * (@ (bK,Z)) by FIELD_6:16;
then aK + (x1 * bK) = (@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z))) by I, FIELD_6:15;
then (@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z))) in FAdj (F,{a,b}) ;
then {((@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z))))} c= the carrier of (FAdj (F,{a,b})) by TARSKI:def 1;
hence G is Subfield of FAdj (F,{a,b}) by H, U, FIELD_6:37; :: thesis:

end;

then reconsider K = FAdj (F,{a,b}) as G -extending FieldExtension of F by FIELD_4:7;
reconsider Z = Z as G -extending K -extending FieldExtension of F by FIELD_4:7;
reconsider aK = aK, bK = bK as Element of K ;
( {((@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z))))} is Subset of G & (@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z))) in {((@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z))))} ) by FIELD_6:35, TARSKI:def 1;
then reconsider lZ = (@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z))) as G -membered Element of Z by FIELD_7:def 5;
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring G) by FIELD_4:10;
then ( MinPoly (a,F) in the carrier of (Polynom-Ring G) & MinPoly (b,F) in the carrier of (Polynom-Ring G) ) ;
then reconsider maG = MinPoly (a,F), mbG = MinPoly (b,F) as Polynomial of G by POLYNOM3:def 10;
( maG is Element of the carrier of (Polynom-Ring G) & mbG is Element of the carrier of (Polynom-Ring G) ) by POLYNOM3:def 10;
then ( deg maG = deg (MinPoly (a,F)) & deg mbG = deg (MinPoly (b,F)) ) by FIELD_4:20;
then reconsider maG = MinPoly (a,F), mbG = MinPoly (b,F) as non constant Polynomial of G by RING_4:def 4, RATFUNC1:def 2;
set g = <%(@ (G,lZ)),(- (@ (x,G)))%>;
set h = Subst (maG,<%(@ (G,lZ)),(- (@ (x,G)))%>);
reconsider mbZ = mbG, hZ = Subst (maG,<%(@ (G,lZ)),(- (@ (x,G)))%>) as Polynomial of Z by FIELD_4:8;
E: hZ gcd mbZ = X- (@ (bK,Z))

proof

E00: ( deg (MinPoly (b,F)) > 0 & LC (MinPoly (b,F)) = 1. F ) by RING_4:def 4, RATFUNC1:def 7;
H: ( mbZ is Element of the carrier of (Polynom-Ring Z) & F is Subfield of Z ) by FIELD_4:7, POLYNOM3:def 10;
E01: deg mbZ = deg (MinPoly (b,F)) by H, FIELD_4:20;
LC mbZ = LC (MinPoly (b,F)) by FIELD_8:5
.= 1. Z by E00, H, EC_PF_1:def 1 ;
then ( not mbZ is constant & mbZ is monic ) by RING_4:def 4, E01, RATFUNC1:def 2, RATFUNC1:def 7;
then reconsider mbZ = mbZ as Ppoly of Z by V, RING_5:70;

now :: thesis:

let a be Element of Z; :: thesis:
H: mbZ is Element of the carrier of (Polynom-Ring Z) by POLYNOM3:def 10;
assume a is_a_root_of mbZ ; :: thesis:
then 0. Z = eval (mbZ,a) by POLYNOM5:def 7
.= Ext_eval ((MinPoly (b,F)),a) by H, FIELD_4:26 ;
then multiplicity ((MinPoly (b,F)),a) = 1 by mpa1, FIELD_4:def 2;
hence multiplicity (mbZ,a) = 1 by defM; :: thesis:

end;

then reconsider mbZ1 = mbZ as Ppoly of Z,(Roots mbZ) by ZZ1;
mbZ is Element of the carrier of (Polynom-Ring Z) by POLYNOM3:def 10;
then E8: Roots mbZ = Roots (Z,(MinPoly (b,F))) by FIELD_7:13;
E9: Roots (Z,(MinPoly (b,F))) = { a where a is Element of Z : a is_a_root_of MinPoly (b,F),Z } by FIELD_4:def 4;
b = @ (bK,Z) by FIELD_7:def 4;
then Ext_eval ((MinPoly (b,F)),(@ (bK,Z))) = Ext_eval ((MinPoly (b,F)),b) by FIELD_6:11
.= 0. E by FIELD_6:52
.= 0. Z by S, EC_PF_1:def 1 ;
then @ (bK,Z) is_a_root_of MinPoly (b,F),Z by FIELD_4:def 2;
then E4: @ (bK,Z) in Roots mbZ by E8, E9;
H1: ( @ ((@ (G,lZ)),Z) = lZ & G is Subring of Z ) by FIELD_5:12, FIELD_7:def 4;
HH: @ (x,G) = x by FIELD_7:def 4
.= @ (x,Z) by FIELD_7:def 4 ;
H2: @ ((- (@ (x,G))),Z) = - (@ (x,G)) by FIELD_7:def 4
.= - (@ (x,Z)) by H1, HH, FIELD_6:17 ;
H3: ((@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z)))) + ((- (@ (x,Z))) * (@ (bK,Z))) = ((@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z)))) + (- ((@ (x,Z)) * (@ (bK,Z)))) by VECTSP_1:9
.= (@ (aK,Z)) + (((@ (x,Z)) * (@ (bK,Z))) + (- ((@ (x,Z)) * (@ (bK,Z))))) by RLVECT_1:def 3
.= (@ (aK,Z)) + (0. Z) by RLVECT_1:5
.= @ (aK,Z) ;
H5: @ (aK,Z) = a by FIELD_7:def 4;
H4: ( MinPoly (a,F) is Element of the carrier of (Polynom-Ring F) & maG is Element of the carrier of (Polynom-Ring G) & hZ is Element of the carrier of (Polynom-Ring Z) & Subst (maG,<%(@ (G,lZ)),(- (@ (x,G)))%>) is Element of the carrier of (Polynom-Ring G) ) by POLYNOM3:def 10;
then eval (hZ,(@ (bK,Z))) = Ext_eval ((Subst (maG,<%(@ (G,lZ)),(- (@ (x,G)))%>)),(@ (bK,Z))) by FIELD_4:26
.= Ext_eval (maG,(Ext_eval (<%(@ (G,lZ)),(- (@ (x,G)))%>,(@ (bK,Z))))) by extevalsubst
.= Ext_eval (maG,(lZ + ((- (@ (x,Z))) * (@ (bK,Z))))) by H1, H2, exteval2
.= Ext_eval ((MinPoly (a,F)),(@ (aK,Z))) by H3, H4, FIELD_8:6
.= Ext_eval ((MinPoly (a,F)),a) by H5, FIELD_6:11
.= 0. E by FIELD_6:52
.= 0. Z by S, EC_PF_1:def 1 ;
then @ (bK,Z) is_a_root_of hZ by POLYNOM5:def 7;
then @ (bK,Z) in Roots hZ by POLYNOM5:def 10;
then E5: @ (bK,Z) in (Roots mbZ) /\ (Roots hZ) by E4;

E7: now :: thesis:

let d be Element of Z; :: thesis:
assume E10: d in (Roots (Z,(MinPoly (b,F)))) \ {b} ; :: thesis:
E9: ((@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z)))) + ((- (@ (x,Z))) * d) = ((@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z)))) + (- ((@ (x,Z)) * d)) by VECTSP_1:9
.= (@ (aK,Z)) + (((@ (x,Z)) * (@ (bK,Z))) + (- ((@ (x,Z)) * d))) by RLVECT_1:def 3 ;
reconsider maG = maG as Element of the carrier of (Polynom-Ring G) by POLYNOM3:def 10;

now :: thesis:

assume d in Roots hZ ; :: thesis:
then d is_a_root_of hZ by POLYNOM5:def 10;
then 0. Z = eval (hZ,d) by POLYNOM5:def 7
.= Ext_eval ((Subst (maG,<%(@ (G,lZ)),(- (@ (x,G)))%>)),d) by H4, FIELD_4:26
.= Ext_eval (maG,(Ext_eval (<%(@ (G,lZ)),(- (@ (x,G)))%>,d))) by extevalsubst
.= Ext_eval (maG,(lZ + ((- (@ (x,Z))) * d))) by H1, H2, exteval2 ;
then R1: (@ (aK,Z)) + (((@ (x,Z)) * (@ (bK,Z))) + (- ((@ (x,Z)) * d))) is_a_root_of maG,Z by E9, FIELD_4:def 2;
Roots (Z,maG) = { a where a is Element of Z : a is_a_root_of maG,Z } by FIELD_4:def 4;
then (@ (aK,Z)) + (((@ (x,Z)) * (@ (bK,Z))) + (- ((@ (x,Z)) * d))) in Roots (Z,maG) by R1;
then R3: (@ (aK,Z)) + (((@ (x,Z)) * (@ (bK,Z))) + (- ((@ (x,Z)) * d))) in Roots (Z,(MinPoly (a,F))) by FIELD_8:7;
((@ (aK,Z)) + (((@ (x,Z)) * (@ (bK,Z))) + (- ((@ (x,Z)) * d)))) + ((@ (x,Z)) * d) = (((@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z)))) + (- ((@ (x,Z)) * d))) + ((@ (x,Z)) * d) by RLVECT_1:def 3
.= ((@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z)))) + ((- ((@ (x,Z)) * d)) + ((@ (x,Z)) * d)) by RLVECT_1:def 3
.= ((@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z)))) + (0. Z) by RLVECT_1:5 ;
hence contradiction by E10, R3, A; :: thesis:

end;

hence not d in Roots hZ ; :: thesis:

end;

(Roots mbZ) /\ (Roots hZ) = {(@ (bK,Z))}

proof

Z: for o being object st o in {(@ (bK,Z))} holds
o in (Roots mbZ) /\ (Roots hZ) by E5, TARSKI:def 1;

now :: thesis:

let o be object ; :: thesis:
assume Z0: o in (Roots mbZ) /\ (Roots hZ) ; :: thesis:
then reconsider z = o as Element of Z ;
Z1: ( z in Roots (Z,(MinPoly (b,F))) & z in Roots hZ ) by Z0, E8, XBOOLE_0:def 4;
then not z in (Roots (Z,(MinPoly (b,F)))) \ {b} by E7;
then z in {b} by Z1, XBOOLE_0:def 5;
then z = b by TARSKI:def 1
.= @ (bK,Z) by FIELD_7:def 4 ;
hence o in {(@ (bK,Z))} by TARSKI:def 1; :: thesis:

end;

hence (Roots mbZ) /\ (Roots hZ) = {(@ (bK,Z))} by Z, TARSKI:2; :: thesis:

end;

then E6: mbZ1 gcd hZ is Ppoly of Z,{(@ (bK,Z))} by simpAgcd;
set gZ = mbZ1 gcd hZ;
deg (mbZ1 gcd hZ) = card {(@ (bK,Z))} by E6, RING_5:60
.= 1 by CARD_2:42 ;
then consider x, z being Element of Z such that
E7: ( x <> 0. Z & mbZ1 gcd hZ = x * (rpoly (1,z)) ) by HURWITZ:28;
E8: 1. Z = LC (mbZ1 gcd hZ) by RATFUNC1:def 7
.= x * (LC (rpoly (1,z))) by E7, RING_5:5
.= x * (1. Z) by RATFUNC1:def 7 ;
E9: Roots (mbZ1 gcd hZ) = {(@ (bK,Z))} by E6, RING_5:63;
eval ((x * (rpoly (1,z))),z) = z - z by E8, HURWITZ:29
.= 0. Z by RLVECT_1:15 ;
then z is_a_root_of x * (rpoly (1,z)) by POLYNOM5:def 7;
then z in Roots (mbZ1 gcd hZ) by E7, POLYNOM5:def 10;
then z = @ (bK,Z) by E9, TARSKI:def 1;
hence hZ gcd mbZ = X- (@ (bK,Z)) by E7, E8, FIELD_9:def 2; :: thesis:

end;

F: b in G

proof

( hZ is Element of the carrier of (Polynom-Ring Z) & mbZ is Element of the carrier of (Polynom-Ring Z) & Subst (maG,<%(@ (G,lZ)),(- (@ (x,G)))%>) is Element of the carrier of (Polynom-Ring G) & mbG is Element of the carrier of (Polynom-Ring G) ) by POLYNOM3:def 10;
then hZ gcd mbZ = (Subst (maG,<%(@ (G,lZ)),(- (@ (x,G)))%>)) gcd mbG by lemgcd;
then reconsider v = X- (@ (bK,Z)) as Polynomial of G by E;
G1: ( @ (bK,Z) = bK & K is Subring of Z & K is Subring of E ) by FIELD_4:def 1, FIELD_7:def 4, FIELD_5:12;
G is Subfield of K by FIELD_4:7;
then G is Subfield of E by EC_PF_1:5;
then G2: G is Subring of E by FIELD_5:12;
v . 0 = (rpoly (1,(@ (bK,Z)))) . 0 by FIELD_9:def 2
.= - ((power Z) . ((@ (bK,Z)),(1 + 0))) by HURWITZ:25
.= - (((power Z) . ((@ (bK,Z)),0)) * (@ (bK,Z))) by GROUP_1:def 7
.= - ((1_ Z) * (@ (bK,Z))) by GROUP_1:def 7
.= - bK by G1, FIELD_6:17
.= - b by G1, FIELD_6:17 ;
then reconsider u = - b as Element of G ;
- u = - (- b) by G2, FIELD_6:17;
hence b in G ; :: thesis:

end;

G: a in G

proof

( {lZ} is Subset of G & lZ in {lZ} ) by TARSKI:def 1, FIELD_6:35;
then reconsider bG = b, lG = lZ as Element of G by F;
H1: G is Subring of Z by FIELD_5:12;
H2: @ (bK,Z) = bG by FIELD_7:def 4;
@ (x,Z) = x by FIELD_7:def 4
.= @ (x,G) by FIELD_7:def 4 ;
then (@ (x,Z)) * (@ (bK,Z)) = (@ (x,G)) * bG by H1, H2, FIELD_6:16;
then - ((@ (x,Z)) * (@ (bK,Z))) = - ((@ (x,G)) * bG) by H1, FIELD_6:17;
then lG - ((@ (x,G)) * bG) = ((@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z)))) + (- ((@ (x,Z)) * (@ (bK,Z)))) by H1, FIELD_6:15
.= (@ (aK,Z)) + (((@ (x,Z)) * (@ (bK,Z))) + (- ((@ (x,Z)) * (@ (bK,Z))))) by RLVECT_1:def 3
.= (@ (aK,Z)) + (0. Z) by RLVECT_1:5
.= a by FIELD_7:def 4 ;
hence a in G ; :: thesis:

end;

G is Subfield of K by FIELD_4:7;
then ( {a,b} c= the carrier of G & G is Subfield of E & F is Subfield of G ) by F, G, TARSKI:def 2, FIELD_4:7, EC_PF_1:5;
then C: FAdj (F,{a,b}) == G by B, FIELD_6:37;
a + ((@ (x,E)) * b) = (@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z)))

proof

E is Subfield of Z by FIELD_4:7;
then D1: E is Subring of Z by FIELD_5:12;
D2: @ (x,E) = x by FIELD_7:def 4
.= @ (x,Z) by FIELD_7:def 4 ;
D3: ( @ (bK,Z) = b & @ (aK,Z) = a ) by FIELD_7:def 4;
(@ (x,E)) * b = (@ (x,Z)) * (@ (bK,Z)) by D1, D2, D3, FIELD_6:16;
hence a + ((@ (x,E)) * b) = (@ (aK,Z)) + ((@ (x,Z)) * (@ (bK,Z))) by D3, D1, FIELD_6:15; :: thesis:

end;

then FAdj (F,{a,b}) = FAdj (F,{(a + ((@ (x,E)) * b))}) by C, FIELD_13:19;
hence ex x being Element of F st FAdj (F,{a,b}) = FAdj (F,{(a + ((@ (x,E)) * b))}) ; :: thesis: