let E be F -algebraic FieldExtension of F; :: thesis: E is F -separable

now :: thesis: for a being Element of E holds a is F -separable

let a be Element of E; :: thesis: a is F -separable
MinPoly (a,F) is separable by dpf;
hence a is F -separable ; :: thesis: verum

end;

hence E is F -separable ; :: thesis: verum