let F be Field; :: thesis: 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 F -fixing Homomorphism of E,K holds (PolyHom h) . p = p
let E be FieldExtension of F; :: thesis: for K being FieldExtension of E
for p being Element of the carrier of (Polynom-Ring F)
for h being F -fixing Homomorphism of E,K holds (PolyHom h) . p = p
let K be FieldExtension of E; :: thesis: for p being Element of the carrier of (Polynom-Ring F)
for h being F -fixing Homomorphism of E,K holds (PolyHom h) . p = p
let p be Element of the carrier of (Polynom-Ring F); :: thesis: for h being F -fixing Homomorphism of E,K holds (PolyHom h) . p = p
let h be F -fixing Homomorphism of E,K; :: thesis: (PolyHom h) . p = p
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring E) by FIELD_4:10;
then reconsider p1 = p as Element of the carrier of (Polynom-Ring E) ;
set g = (PolyHom h) . p1;
H: dom ((PolyHom h) . p1) = NAT by FUNCT_2:def 1
.= dom p by FUNCT_2:def 1 ;

now :: thesis: for o being object st o in dom ((PolyHom h) . p1) holds
((PolyHom h) . p1) . o = p . o

let o be object ; :: thesis: ( o in dom ((PolyHom h) . p1) implies ((PolyHom h) . p1) . o = p . o )
assume o in dom ((PolyHom h) . p1) ; :: thesis: ((PolyHom h) . p1) . o = p . o
then reconsider i = o as Nat ;
((PolyHom h) . p1) . i = h . (p1 . i) by FIELD_1:def 2
.= p . i by FIELD_8:def 2 ;
hence ((PolyHom h) . p1) . o = p . o ; :: thesis: verum

end;

hence (PolyHom h) . p = p by H, FUNCT_1:2; :: thesis: verum