theorem lemNor3e: :: FIELD_13:26

for F1 being Field
for F2 being b₁ -homomorphic b₁ -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)) . a = b