let L be non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of L holds p *' <%(1. L)%> = p
let p be Polynomial of L; :: thesis: p *' <%(1. L)%> = p
thus p *' <%(1. L)%> = p *' (1_. L) by Th28
.= p by POLYNOM3:35 ; :: thesis: verum