let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) ex E being FieldExtension of F st E is SplittingField of p
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ex E being FieldExtension of F st E is SplittingField of p
set E = the SplittingField of p;
take the SplittingField of p ; :: thesis: the SplittingField of p is SplittingField of p
thus the SplittingField of p is SplittingField of p ; :: thesis: verum