let n be Nat; :: thesis: for R being non degenerated Ring
for a being Element of R holds LC (anpoly (a,n)) = a
let R be non degenerated Ring; :: thesis: for a being Element of R holds LC (anpoly (a,n)) = a
let a be Element of R; :: thesis: LC (anpoly (a,n)) = a
set q = anpoly (a,n);

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

suppose A1: a = 0. R ; :: thesis: LC (anpoly (a,n)) = a

then anpoly (a,n) = 0_. R by UPROOTS:def 5;
then (anpoly (a,n)) . ((len (anpoly (a,n))) -' 1) = 0. R by FUNCOP_1:7;
hence LC (anpoly (a,n)) = a by A1, RATFUNC1:def 6; :: thesis: verum

end;

suppose a <> 0. R ; :: thesis: LC (anpoly (a,n)) = a

then not a is zero ;
then A2: n = deg (anpoly (a,n)) by Lm1
.= (len (anpoly (a,n))) - 1 ;
then n + 1 = len (anpoly (a,n)) ;
then (len (anpoly (a,n))) -' 1 = n by A2, XREAL_1:233, NAT_1:11;
hence a = (anpoly (a,n)) . ((len (anpoly (a,n))) -' 1) by POLYDIFF:24
.= LC (anpoly (a,n)) by RATFUNC1:def 6 ;
:: thesis: verum

end;

end;