let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for p, q being Polynomial of L holds
( p divides q iff ex r being Polynomial of L st p *' r = q )
let p, q be Polynomial of L; :: thesis: ( p divides q iff ex r being Polynomial of L st p *' r = q )
X: now :: thesis: ( p divides q implies ex r being Polynomial of L st p *' r = q )
assume p divides q ; :: thesis: ex r being Polynomial of L st p *' r = q
then consider a, b being Element of (Polynom-Ring L) such that
B: ( a = p & b = q & a divides b ) ;
consider u being Element of (Polynom-Ring L) such that
C: a * u = b by B;
reconsider z = u as Polynomial of L by POLYNOM3:def 10;
q = p *' z by B, C, POLYNOM3:def 10;
hence ex r being Polynomial of L st p *' r = q ; :: thesis: verum
end;
now :: thesis: ( ex r being Polynomial of L st p *' r = q implies p divides q )
assume ex r being Polynomial of L st p *' r = q ; :: thesis: p divides q
then consider r being Polynomial of L such that
H: q = p *' r ;
reconsider a = p, b = q, u = r as Element of (Polynom-Ring L) by POLYNOM3:def 10;
b = a * u by H, POLYNOM3:def 10;
then a divides b ;
hence p divides q ; :: thesis: verum
end;
hence ( p divides q iff ex r being Polynomial of L st p *' r = q ) by X; :: thesis: verum