let R be non degenerated Ring; :: thesis: for S being RingExtension of R
for p being Polynomial of R
for q being Polynomial of S st p = q holds
LC p = LC q
let S be RingExtension of R; :: thesis: for p being Polynomial of R
for q being Polynomial of S st p = q holds
LC p = LC q
let p be Polynomial of R; :: thesis: for q being Polynomial of S st p = q holds
LC p = LC q
let q be Polynomial of S; :: thesis: ( p = q implies LC p = LC q )
assume A: p = q ; :: thesis: LC p = LC q
H: R is Subring of S by FIELD_4:def 1;

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

suppose C: p = 0_. R ; :: thesis: LC p = LC q

D: LC p = p . ((len p) -' 1) by RATFUNC1:def 6
.= 0. S by C, H, C0SP1:def 3 ;
E: q = 0_. S by A, C, FIELD_4:12;
thus LC q = q . ((len q) -' 1) by RATFUNC1:def 6
.= LC p by D, E ; :: thesis: verum

end;

suppose F: p <> 0_. R ; :: thesis: LC p = LC q

then C: not p is zero by UPROOTS:def 5;

D: now :: thesis: not q is zero

assume q is zero ; :: thesis: contradiction
then q = 0_. S by UPROOTS:def 5
.= 0_. R by FIELD_4:12 ;
hence contradiction by A, F; :: thesis: verum

end;

E: ( p is Element of the carrier of (Polynom-Ring R) & q is Element of the carrier of (Polynom-Ring S) ) by POLYNOM3:def 10;
thus LC p = p . (deg p) by C, FIELD_6:2
.= q . (deg q) by A, E, FIELD_4:20
.= LC q by D, FIELD_6:2 ; :: thesis: verum

end;

end;