let L be non degenerated right_complementable add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for p being Polynomial of L holds LC p = - (LC (- p))
let p be Polynomial of L; :: thesis: LC p = - (LC (- p))
A1: len p = len (- p) by POLYNOM4:8;
A2: dom (- p) = NAT by FUNCT_2:def 1;
thus LC p = - (- (p /. ((len p) -' 1)))
.= - ((- p) /. ((len (- p)) -' 1)) by A1, A2, VFUNCT_1:def 5
.= - (LC (- p)) ; :: thesis: verum