let R be domRing; :: thesis: for f, g being Element of the carrier of (Polynom-Ring R)
for a being Element of R st f = a | R holds
(Der1 R) . (f * g) = (a | R) *' ((Der1 R) . g)
let f, g be Element of the carrier of (Polynom-Ring R); :: thesis: for a being Element of R st f = a | R holds
(Der1 R) . (f * g) = (a | R) *' ((Der1 R) . g)
let a be Element of R; :: thesis: ( f = a | R implies (Der1 R) . (f * g) = (a | R) *' ((Der1 R) . g) )
assume A1: f = a | R ; :: thesis: (Der1 R) . (f * g) = (a | R) *' ((Der1 R) . g)
reconsider f1 = f, g1 = g as sequence of R ;
reconsider f9 = f, g9 = g as Polynomial of R ;
reconsider fg0 = f * g as Element of (Polynom-Ring R) ;
reconsider fg9 = f9 *' g9 as Element of (Polynom-Ring R) by POLYNOM3:def 10;
reconsider fg1 = f1 *' g1 as sequence of R ;
A2: f * g = (a | R) *' g9 by A1, POLYNOM3:def 10;
for n being Nat holds ((Der1 R) . (f * g)) . n = ((a | R) *' ((Der1 R) . g)) . n

proof

let n be Nat; :: thesis: ((Der1 R) . (f * g)) . n = ((a | R) *' ((Der1 R) . g)) . n
reconsider b = g9 . (n + 1) as Element of R ;
reconsider Dg = (Der1 R) . g as Polynomial of R ;
((Der1 R) . (f * g)) . n = (n + 1) * (((a | R) *' g9) . (n + 1)) by A2, Def8
.= (n + 1) * (a * (g9 . (n + 1))) by Th27
.= a * ((n + 1) * (g9 . (n + 1))) by BINOM:19
.= a * (((Der1 R) . g) . n) by Def8
.= ((a | R) *' ((Der1 R) . g)) . n by Th27 ;
hence ((Der1 R) . (f * g)) . n = ((a | R) *' ((Der1 R) . g)) . n ; :: thesis: verum

end;

hence (Der1 R) . (f * g) = (a | R) *' ((Der1 R) . g) ; :: thesis: verum