let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed 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 A: a = 0. L ; :: thesis: LC (a * p) = a * (LC p)

then B: a * (LC p) = 0. L by VECTSP_1:6;
a * p = 0_. L by A, POLYNOM5:26;
hence LC (a * p) = a * (LC p) by B, FUNCOP_1:7; :: thesis: verum

end;

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

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

end;

end;