let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E holds multiplicity (p,a) <= 1 ) ) )
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( p is separable iff ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E holds multiplicity (p,a) <= 1 ) ) )

A: now :: thesis: ( p is separable implies ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E holds multiplicity (p,a) <= 1 ) ) )

assume AS: p is separable ; :: thesis: ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E holds multiplicity (p,a) <= 1 ) )
set K = the SplittingField of p;
B: p splits_in the SplittingField of p by FIELD_8:def 1;
for a being Element of the SplittingField of p holds multiplicity (p,a) <= 1 by AS, ThSep01;
hence ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E holds multiplicity (p,a) <= 1 ) ) by B; :: thesis: verum

end;

now :: thesis: ( ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E holds multiplicity (p,a) <= 1 ) ) implies p is separable )

assume ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E holds multiplicity (p,a) <= 1 ) ) ; :: thesis: p is separable
then consider E being FieldExtension of F such that
AS: ( p splits_in E & ( for a being Element of E holds multiplicity (p,a) <= 1 ) ) ;

now :: thesis: for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1

let a be Element of E; :: thesis: ( a is_a_root_of p,E implies multiplicity (p,a) = 1 )
assume a is_a_root_of p,E ; :: thesis: multiplicity (p,a) = 1
then ( multiplicity (p,a) >= 1 & multiplicity (p,a) <= 1 ) by AS, mulzero;
hence multiplicity (p,a) = 1 by XXREAL_0:1; :: thesis: verum

end;

hence p is separable by AS, ThSep1; :: thesis: verum

end;

hence ( p is separable iff ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E holds multiplicity (p,a) <= 1 ) ) ) by A; :: thesis: verum