let L be non empty right_complementable distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for p, q, r being Polynomial of L st p <> 0_. L & p *' q = p *' r holds

q = r

let p, q, r be Polynomial of L; :: thesis: ( p <> 0_. L & p *' q = p *' r implies q = r )

assume A1: p <> 0_. L ; :: thesis: ( not p *' q = p *' r or q = r )

assume p *' q = p *' r ; :: thesis: q = r

then (p *' q) - (p *' r) = 0_. L by POLYNOM3:29;

then p *' (q - r) = 0_. L by Th23;

then q - r = 0_. L by A1, Th18;

hence q = r by Th24; :: thesis: verum

q = r

let p, q, r be Polynomial of L; :: thesis: ( p <> 0_. L & p *' q = p *' r implies q = r )

assume A1: p <> 0_. L ; :: thesis: ( not p *' q = p *' r or q = r )

assume p *' q = p *' r ; :: thesis: q = r

then (p *' q) - (p *' r) = 0_. L by POLYNOM3:29;

then p *' (q - r) = 0_. L by Th23;

then q - r = 0_. L by A1, Th18;

hence q = r by Th24; :: thesis: verum