let R be Ring; :: thesis: for a being Element of R holds LC (a | R) = a
let a be Element of R; :: thesis: LC (a | R) = a
H: ( 0 - 1 < 0 & 1 - 1 >= 0 ) ;

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

suppose A: a = 0. R ; :: thesis: LC (a | R) = a

then B: a | R = 0_. R by RING_4:13;
then len (a | R) = 0 by POLYNOM4:3;
then (len (a | R)) -' 1 = 0 by H, XREAL_0:def 2;
then LC (a | R) = (a | R) . 0 by RATFUNC1:def 6;
hence LC (a | R) = a by A, B; :: thesis: verum

end;

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

then A: deg (a | R) = 0 by RING_4:21;
deg (a | R) = (len (a | R)) - 1 by HURWITZ:def 2;
then (len (a | R)) -' 1 = 0 by A, XREAL_0:def 2;
then LC (a | R) = (a | R) . 0 by RATFUNC1:def 6;
hence LC (a | R) = a by poly0; :: thesis: verum

end;

end;