let F1 be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1, E2 being SplittingField of p ex h being Function of E1,E2 st h is F1 -isomorphism
let p be non constant Element of the carrier of (Polynom-Ring F1); :: thesis: for E1, E2 being SplittingField of p ex h being Function of E1,E2 st h is F1 -isomorphism
let E1, E be SplittingField of p; :: thesis: ex h being Function of E1,E st h is F1 -isomorphism
id F1 is isomorphism ;
then reconsider F2 = F1 as F1 -homomorphic F1 -isomorphic Field by RING_2:def 4, RING_3:def 4;
reconsider h = id F1 as Isomorphism of F1,F2 ;

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

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

end;

then (PolyHom h) . p = p ;
then reconsider E2 = E as SplittingField of (PolyHom h) . p ;
consider f being Function of E1,E2 such that
B: ( f is h -extending & f is isomorphism ) by unique2;
reconsider f = f as Function of E1,E ;
take f ; :: thesis: f is F1 -isomorphism

now :: thesis: for a being Element of F1 holds f . a = a

let a be Element of F1; :: thesis: f . a = a
thus f . a = h . a by B
.= a ; :: thesis: verum

end;

then f is F1 -fixing ;
hence f is F1 -isomorphism by B, deffixiso; :: thesis: verum