let F be Field; :: thesis: for p, q being non constant Element of the carrier of (Polynom-Ring F)
for r being Element of the carrier of (Polynom-Ring F) st p = q *' r & p is separable holds
q is separable
let p, q be non constant Element of the carrier of (Polynom-Ring F); :: thesis: for r being Element of the carrier of (Polynom-Ring F) st p = q *' r & p is separable holds
q is separable
let r be Element of the carrier of (Polynom-Ring F); :: thesis: ( p = q *' r & p is separable implies q is separable )
assume A: p = q *' r ; :: thesis: ( not p is separable or q is separable )
assume B: p is separable ; :: thesis: q is separable
reconsider r = r as non zero Polynomial of F by A;

now :: thesis: not q is inseparable

assume q is inseparable ; :: thesis: contradiction
then consider E being FieldExtension of F such that
D: not for a being Element of E holds multiplicity (q,a) <= 1 by ThSep02;
consider a being Element of E such that
E: multiplicity (q,a) > 1 by D;
F: multiplicity (p,a) = (multiplicity (q,a)) + (multiplicity (r,a)) by A, UP55;
(multiplicity (q,a)) + (multiplicity (r,a)) >= multiplicity (q,a) by NAT_1:11;
then multiplicity (p,a) > 1 by F, E, XXREAL_0:2;
hence contradiction by B, ThSep02; :: thesis: verum

end;

hence q is separable ; :: thesis: verum