let F1 be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F1)
for F2 being F1 -isomorphic Field
for h being Isomorphism of F1,F2 holds
( p splits_in F1 iff (PolyHom h) . p splits_in F2 )
let p be non constant Element of the carrier of (Polynom-Ring F1); :: thesis: for F2 being F1 -isomorphic Field
for h being Isomorphism of F1,F2 holds
( p splits_in F1 iff (PolyHom h) . p splits_in F2 )
let F2 be F1 -isomorphic Field; :: thesis: for h being Isomorphism of F1,F2 holds
( p splits_in F1 iff (PolyHom h) . p splits_in F2 )
let h be Isomorphism of F1,F2; :: thesis: ( p splits_in F1 iff (PolyHom h) . p splits_in F2 )

now :: thesis: ( (PolyHom h) . p splits_in F2 implies p splits_in F1 )

assume AS: (PolyHom h) . p splits_in F2 ; :: thesis: p splits_in F1
h " is Isomorphism of F2,F1 by RING_3:73;
then reconsider F1a = F1 as F2 -homomorphic F2 -isomorphic Field by RING_3:def 4, RING_2:def 4;
reconsider g = h " as Isomorphism of F2,F1a by RING_3:73;

now :: thesis: for i being Element of NAT holds ((PolyHom g) . ((PolyHom h) . p)) . i = p . i

let i be Element of NAT ; :: thesis: ((PolyHom g) . ((PolyHom h) . p)) . i = p . i
thus ((PolyHom g) . ((PolyHom h) . p)) . i = g . (((PolyHom h) . p) . i) by FIELD_1:def 2
.= g . (h . (p . i)) by FIELD_1:def 2
.= p . i by FUNCT_2:26 ; :: thesis: verum

end;

then (PolyHom g) . ((PolyHom h) . p) = p ;
hence p splits_in F1 by AS, lemma6a; :: thesis: verum

end;

hence ( p splits_in F1 iff (PolyHom h) . p splits_in F2 ) by lemma6a; :: thesis: verum