let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for p, q, r being Polynomial of L holds (p *' q) - (p *' r) = p *' (q - r)
let p, q, r be Polynomial of L; :: thesis: (p *' q) - (p *' r) = p *' (q - r)
set PRL = Polynom-Ring L;
reconsider pc = p, qc = q, rc = r as Element of (Polynom-Ring L) by POLYNOM3:def 12;
A1: p *' q = pc * qc by POLYNOM3:def 12;
A2: p *' r = pc * rc by POLYNOM3:def 12;
A3: qc - rc = q - r by Th27;
thus (p *' q) - (p *' r) = (pc * qc) - (pc * rc) by A1, A2, Th27
.= pc * (qc - rc) by VECTSP_1:43
.= p *' (q - r) by A3, POLYNOM3:def 12 ; :: thesis: verum