let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F)
for E1, E2 being SplittingField of p holds E1,E2 are_isomorphic_over F
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: for E1, E2 being SplittingField of p holds E1,E2 are_isomorphic_over F
let E1, E2 be SplittingField of p; :: thesis: E1,E2 are_isomorphic_over F
consider f being Function of E1,E2 such that
A: f is F -isomorphism by unique3;
thus E1,E2 are_isomorphic_over F by A; :: thesis: verum