let F be non degenerated comRing; :: thesis: for p being Element of the carrier of (Polynom-Ring F)
for S being comRingExtension of F
for q being Element of the carrier of (Polynom-Ring S) st q = p holds
(Deriv S) . q = (Deriv F) . p
let p be Element of the carrier of (Polynom-Ring F); :: thesis: for S being comRingExtension of F
for q being Element of the carrier of (Polynom-Ring S) st q = p holds
(Deriv S) . q = (Deriv F) . p
let E be comRingExtension of F; :: thesis: for q being Element of the carrier of (Polynom-Ring E) st q = p holds
(Deriv E) . q = (Deriv F) . p
let q be Element of the carrier of (Polynom-Ring E); :: thesis: ( q = p implies (Deriv E) . q = (Deriv F) . p )
assume AS: q = p ; :: thesis: (Deriv E) . q = (Deriv F) . p
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring E) by FIELD_4:10;
then reconsider p1 = (Deriv F) . p as Element of the carrier of (Polynom-Ring E) ;

now :: thesis: for o being object st o in NAT holds
((Deriv E) . q) . o = p1 . o

let o be object ; :: thesis: ( o in NAT implies ((Deriv E) . q) . o = p1 . o )
assume o in NAT ; :: thesis: ((Deriv E) . q) . o = p1 . o
then reconsider i = o as Element of NAT ;
((Deriv E) . q) . i = (i + 1) * (q . (i + 1)) by RINGDER1:def 8
.= (i + 1) * (p . (i + 1)) by AS, mm5a
.= p1 . i by RINGDER1:def 8 ;
hence ((Deriv E) . q) . o = p1 . o ; :: thesis: verum

end;

hence (Deriv E) . q = (Deriv F) . p by FUNCT_2:12; :: thesis: verum