let F1 be Field; :: thesis: for F2 being F1 -homomorphic F1 -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
let F2 be F1 -homomorphic F1 -isomorphic Field; :: thesis: for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
let h be Isomorphism of F1,F2; :: thesis: for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
let E1 be FieldExtension of F1; :: thesis: for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
let E2 be FieldExtension of F2; :: thesis: for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
let a be Element of E1; :: thesis: for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
let b be Element of E2; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
let p be irreducible Element of the carrier of (Polynom-Ring F1); :: thesis: ( Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 implies ( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism ) )
assume AS: ( Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 ) ; :: thesis: ( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
set f = Psi (a,b,h,p);
set C1 = the carrier of (FAdj (F1,{a}));
set C2 = the carrier of (FAdj (F2,{b}));
reconsider a = a as F1 -algebraic Element of E1 by AS, FIELD_6:43;
H1: FAdj (F1,{a}) = RAdj (F1,{a}) by FIELD_6:56;
H2: the carrier of (RAdj (F1,{a})) = { (Ext_eval (p,a)) where p is Polynomial of F1 : verum } by FIELD_6:45;
reconsider b = b as F2 -algebraic Element of E2 by AS, FIELD_6:43;

now :: thesis: for x being Element of F1 holds (Psi (a,b,h,p)) . x = h . x

let x be Element of F1; :: thesis: (Psi (a,b,h,p)) . x = h . x
reconsider g1 = x | F1 as Element of the carrier of (Polynom-Ring F1) by POLYNOM3:def 10;
H6: the carrier of (Polynom-Ring F2) c= the carrier of (Polynom-Ring E2) by FIELD_4:10;
(h . x) | F2 is Element of the carrier of (Polynom-Ring F2) by POLYNOM3:def 10;
then reconsider g2 = (h . x) | F2 as Element of the carrier of (Polynom-Ring E2) by H6;
x = Ext_eval ((x | F1),a) by u3;
hence (Psi (a,b,h,p)) . x = Ext_eval (((PolyHom h) . g1),b) by AS, psi
.= Ext_eval (((h . x) | F2),b) by hcon
.= LC ((h . x) | F2) by FIELD_6:28
.= h . x by hcon2 ;
:: thesis: verum

end;

hence Psi (a,b,h,p) is h -extending ; :: thesis: Psi (a,b,h,p) is isomorphism
set F1a = FAdj (F1,{a});
set F2b = FAdj (F2,{b});
reconsider f = Psi (a,b,h,p) as Function of (FAdj (F1,{a})),(FAdj (F2,{b})) ;
A: f . (1. (FAdj (F1,{a}))) = 1. (FAdj (F2,{b}))

proof

( F1 is Subfield of FAdj (F1,{a}) & F2 is Subfield of FAdj (F2,{b}) ) by FIELD_6:36;
then A0: ( 1. (FAdj (F1,{a})) = 1. F1 & 1. (FAdj (F2,{b})) = 1. F2 ) by EC_PF_1:def 1;
A1: 1_. (FAdj (F1,{a})) = 1_. F1 by FIELD_4:14;
A2: (PolyHom h) . (1_. (FAdj (F1,{a}))) = (PolyHom h) . (1_. F1) by FIELD_4:14
.= (PolyHom h) . ((1. F1) | F1) by RING_4:14
.= (h . (1_ F1)) | F2 by hcon
.= (1_ F2) | F2 by GROUP_1:def 13
.= (1. (FAdj (F2,{b}))) | (FAdj (F2,{b})) by A0, FIELD_6:23
.= 1_. (FAdj (F2,{b})) by RING_4:14 ;
reconsider r = 1_. (FAdj (F1,{a})) as Element of the carrier of (Polynom-Ring F1) by A1, POLYNOM3:def 10;
thus f . (1. (FAdj (F1,{a}))) = f . (Ext_eval (r,a)) by A1, u1
.= Ext_eval (((PolyHom h) . r),b) by AS, psi
.= Ext_eval ((1_. F2),b) by A2, FIELD_4:14
.= 1. (FAdj (F2,{b})) by u1 ; :: thesis: verum

end;

B: now :: thesis: for x, y being Element of (FAdj (F1,{a})) holds f . (x * y) = (f . x) * (f . y)

let x, y be Element of (FAdj (F1,{a})); :: thesis: f . (x * y) = (f . x) * (f . y)
x in { (Ext_eval (p,a)) where p is Polynomial of F1 : verum } by H1, H2;
then consider r1 being Polynomial of F1 such that
B1: x = Ext_eval (r1,a) ;
y in { (Ext_eval (p,a)) where p is Polynomial of F1 : verum } by H1, H2;
then consider r2 being Polynomial of F1 such that
B2: y = Ext_eval (r2,a) ;
reconsider q1 = r1, q2 = r2 as Element of the carrier of (Polynom-Ring F1) by POLYNOM3:def 10;
B3: q1 * q2 = r1 *' r2 by POLYNOM3:def 10;
reconsider g1 = (PolyHom h) . q1, g2 = (PolyHom h) . q2 as Polynomial of F2 ;
B4: g1 *' g2 = ((PolyHom h) . q1) * ((PolyHom h) . q2) by POLYNOM3:def 10;
B5: ( f . x = Ext_eval (g1,b) & f . y = Ext_eval (g2,b) ) by B1, B2, AS, psi;
thus f . (x * y) = f . (Ext_eval ((r1 *' r2),a)) by u2, B1, B2
.= Ext_eval (((PolyHom h) . (q1 * q2)),b) by B3, AS, psi
.= Ext_eval ((g1 *' g2),b) by B4, FIELD_1:25
.= (f . x) * (f . y) by u2, B5 ; :: thesis: verum

end;

C: now :: thesis: for x, y being Element of (FAdj (F1,{a})) holds f . (x + y) = (f . x) + (f . y)

let x, y be Element of (FAdj (F1,{a})); :: thesis: f . (x + y) = (f . x) + (f . y)
x in { (Ext_eval (p,a)) where p is Polynomial of F1 : verum } by H1, H2;
then consider r1 being Polynomial of F1 such that
B1: x = Ext_eval (r1,a) ;
y in { (Ext_eval (p,a)) where p is Polynomial of F1 : verum } by H1, H2;
then consider r2 being Polynomial of F1 such that
B2: y = Ext_eval (r2,a) ;
reconsider q1 = r1, q2 = r2 as Element of the carrier of (Polynom-Ring F1) by POLYNOM3:def 10;
reconsider q = q1 + q2 as Element of the carrier of (Polynom-Ring F1) ;
B3: q1 + q2 = r1 + r2 by POLYNOM3:def 10;
reconsider g1 = (PolyHom h) . q1, g2 = (PolyHom h) . q2 as Polynomial of F2 ;
B4: g1 + g2 = ((PolyHom h) . q1) + ((PolyHom h) . q2) by POLYNOM3:def 10
.= (PolyHom h) . (q1 + q2) by FIELD_1:24 ;
B5: ( f . x = Ext_eval (g1,b) & f . y = Ext_eval (g2,b) ) by B1, B2, AS, psi;
thus f . (x + y) = f . (Ext_eval ((r1 + r2),a)) by u2, B1, B2
.= Ext_eval (((PolyHom h) . q),b) by B3, AS, psi
.= (f . x) + (f . y) by u2, B4, B5 ; :: thesis: verum

end;

D: f is onto

proof

E1: now :: thesis: for o being object st o in rng f holds
o in the carrier of (FAdj (F2,{b}))

let o be object ; :: thesis: ( o in rng f implies o in the carrier of (FAdj (F2,{b})) )
assume E2: o in rng f ; :: thesis: o in the carrier of (FAdj (F2,{b}))
rng f c= the carrier of (FAdj (F2,{b})) by RELAT_1:def 19;
hence o in the carrier of (FAdj (F2,{b})) by E2; :: thesis: verum

end;

I2: ( FAdj (F1,{a}) = RAdj (F1,{a}) & FAdj (F2,{b}) = RAdj (F2,{b}) ) by FIELD_6:56;

now :: thesis: for o being object st o in the carrier of (FAdj (F2,{b})) holds
o in rng f

let o be object ; :: thesis: ( o in the carrier of (FAdj (F2,{b})) implies o in rng f )
assume o in the carrier of (FAdj (F2,{b})) ; :: thesis: o in rng f
then o in { (Ext_eval (p,b)) where p is Polynomial of F2 : verum } by I2, FIELD_6:45;
then consider p being Polynomial of F2 such that
E2: o = Ext_eval (p,b) ;
PolyHom h is onto ;
then p in rng (PolyHom h) by POLYNOM3:def 10;
then consider ph being object such that
E3: ( ph in dom (PolyHom h) & (PolyHom h) . ph = p ) by FUNCT_1:def 3;
reconsider ph = ph as Element of the carrier of (Polynom-Ring F1) by E3;
Ext_eval (ph,a) in { (Ext_eval (p,a)) where p is Polynomial of F1 : verum } ;
then Ext_eval (ph,a) in the carrier of (FAdj (F1,{a})) by I2, FIELD_6:45;
then E4: Ext_eval (ph,a) in dom f by FUNCT_2:def 1;
f . (Ext_eval (ph,a)) = o by E2, E3, AS, psi;
hence o in rng f by E4, FUNCT_1:def 3; :: thesis: verum

end;

hence f is onto by E1, TARSKI:2; :: thesis: verum

end;

( f is additive & f is multiplicative & f is unity-preserving ) by A, B, C;
hence Psi (a,b,h,p) is isomorphism by D; :: thesis: verum