let R be domRing; :: thesis: for p being Polynomial of R
for a being Element of R holds LC (a * p) = a * (LC p)
let p be Polynomial of R; :: thesis: for a being Element of R holds LC (a * p) = a * (LC p)
let a be Element of R; :: thesis: LC (a * p) = a * (LC p)

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

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

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

end;

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

then A3: not a is zero ;
thus LC (a * p) = a * (p . ((len (a * p)) -' 1)) by POLYNOM5:def 4
.= a * (LC p) by A3, Th25a ; :: thesis: verum

end;

end;