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

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