theorem fixp: :: FIELD_13:41

for F being Field
for E being FieldExtension of F
for K being FieldExtension of E
for p being Element of the carrier of (Polynom-Ring F)
for h being b₁ -fixing Homomorphism of E,K holds (PolyHom h) . p = p