set p = the non constant Element of the carrier of (Polynom-Ring F);
set K = the SplittingField of the non constant Element of the carrier of (Polynom-Ring F);
take the SplittingField of the non constant Element of the carrier of (Polynom-Ring F) ; :: thesis: ( the SplittingField of the non constant Element of the carrier of (Polynom-Ring F) is F -normal & the SplittingField of the non constant Element of the carrier of (Polynom-Ring F) is F -separable )
thus ( the SplittingField of the non constant Element of the carrier of (Polynom-Ring F) is F -normal & the SplittingField of the non constant Element of the carrier of (Polynom-Ring F) is F -separable ) ; :: thesis: verum