let L be non trivial right_complementable distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for p1, p2 being Polynomial of L
for p3 being non zero Polynomial of L st p1 *' p3 = p2 *' p3 holds
p1 = p2
let p1, p2 be Polynomial of L; :: thesis: for p3 being non zero Polynomial of L st p1 *' p3 = p2 *' p3 holds
p1 = p2
let p3 be non zero Polynomial of L; :: thesis: ( p1 *' p3 = p2 *' p3 implies p1 = p2 )
assume A1: p1 *' p3 = p2 *' p3 ; :: thesis: p1 = p2
reconsider x1 = p1 as Element of (Polynom-Ring L) by POLYNOM3:def 10;
reconsider x2 = p2 as Element of (Polynom-Ring L) by POLYNOM3:def 10;
reconsider x3 = p3 as Element of (Polynom-Ring L) by POLYNOM3:def 10;
p3 <> 0_. L ;
then A2: x3 <> 0. (Polynom-Ring L) by POLYNOM3:def 10;
A3: x1 * x3 = p2 *' p3 by A1, POLYNOM3:def 10
.= x2 * x3 by POLYNOM3:def 10 ;
x3 is right_mult-cancelable by A2, ALGSTR_0:def 37;
hence p1 = p2 by A3; :: thesis: verum