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