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

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