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 10;
A1: qc - rc = q - r by Th22;
( p *' q = pc * qc & p *' r = pc * rc ) by POLYNOM3:def 10;
hence (p *' q) - (p *' r) = (pc * qc) - (pc * rc) by Th22
.= pc * (qc - rc) by VECTSP_1:11
.= p *' (q - r) by A1, POLYNOM3:def 10 ;
:: thesis: verum