let L be non empty right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for p being Polynomial of L
for a being Element of L holds LC (a * p) = a * (LC p)
let p be Polynomial of L; :: thesis: for a being Element of L holds LC (a * p) = a * (LC p)
let a be Element of L; :: thesis: LC (a * p) = a * (LC p)

per cases ( a = 0. L or a <> 0. L ) ;

suppose A1: a = 0. L ; :: thesis: LC (a * p) = a * (LC p)

then A2: a * (LC p) = 0. L ;
a * p = 0_. L by A1, POLYNOM5:26;
hence LC (a * p) = a * (LC p) by A2, FUNCOP_1:7; :: thesis: verum

end;

suppose A3: a <> 0. L ; :: thesis: LC (a * p) = a * (LC p)

thus LC (a * p) = a * (p . ((len (a * p)) -' 1)) by POLYNOM5:def 4
.= a * (LC p) by A3, POLYNOM5:25 ; :: thesis: verum

end;

end;