let R be domRing; :: thesis: for f, g being Element of the carrier of (Polynom-Ring R) st f = anpoly ((1. R),1) holds
(Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g))
let f, g be Element of the carrier of (Polynom-Ring R); :: thesis: ( f = anpoly ((1. R),1) implies (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g)) )
assume A1: f = anpoly ((1. R),1) ; :: thesis: (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g))
reconsider df1 = (Der1 R) . f, dg1 = (Der1 R) . g as Polynomial of R ;
reconsider f1 = f, g1 = g as Polynomial of R ;
A2: ( df1 *' g1 = ((Der1 R) . f) * g & f1 *' dg1 = f * ((Der1 R) . g) ) by POLYNOM3:def 10;
for i being Element of NAT holds ((Der1 R) . (f * g)) . i = ((df1 *' g1) + (f1 *' dg1)) . i

proof

let i be Element of NAT ; :: thesis: ((Der1 R) . (f * g)) . i = ((df1 *' g1) + (f1 *' dg1)) . i
f * g = f1 *' g1 by POLYNOM3:def 10;
then A3: ((Der1 R) . (f * g)) . i = (i + 1) * ((f1 *' g1) . (i + 1)) by Def8
.= (i + 1) * (g1 . i) by A1, Th31 ;
A4: df1 *' g1 = (anpoly ((1. R),0)) *' g1 by Th30, A1
.= (1_. R) *' g1
.= g1 ;
A5: ((df1 *' g1) + (f1 *' dg1)) . i = (g1 . i) + ((f1 *' dg1) . i) by A4, NORMSP_1:def 2;

per cases ( i > 0 or i <= 1 ) ;

suppose i > 0 ; :: thesis: ((Der1 R) . (f * g)) . i = ((df1 *' g1) + (f1 *' dg1)) . i

then reconsider j = i - 1 as Element of NAT by INT_1:3;
(f1 *' dg1) . (j + 1) = dg1 . j by Th31, A1;
then A8: (f1 *' dg1) . i = i * (g1 . i) by Def8;
f * g = f1 *' g1 by POLYNOM3:def 10;
then ((Der1 R) . (f * g)) . i = (i + 1) * ((f1 *' g1) . (i + 1)) by Def8
.= (i * ((f1 *' g1) . (i + 1))) + (1 * ((f1 *' g1) . (i + 1))) by BINOM:15
.= (i * ((f1 *' g1) . (i + 1))) + ((f1 *' g1) . (i + 1)) by BINOM:13
.= (i * ((f1 *' g1) . (i + 1))) + (g1 . i) by A1, Th31
.= (i * (g1 . i)) + (g1 . i) by A1, Th31 ;
hence ((Der1 R) . (f * g)) . i = ((df1 *' g1) + (f1 *' dg1)) . i by A4, NORMSP_1:def 2, A8; :: thesis: verum

end;

suppose i <= 1 ; :: thesis: ((Der1 R) . (f * g)) . i = ((df1 *' g1) + (f1 *' dg1)) . i

then ( i < 1 or i = 1 ) by XXREAL_0:1;

per cases then ( i = 1 or i = 0 ) by NAT_1:14;

suppose A12: i = 1 ; :: thesis: ((Der1 R) . (f * g)) . i = ((df1 *' g1) + (f1 *' dg1)) . i

(f1 *' dg1) . (0 + 1) = dg1 . 0 by A1, Th31
.= (0 + 1) * (g1 . (0 + 1)) by Def8
.= 1 * (g1 . 1) ;
then ((df1 *' g1) + (f1 *' dg1)) . i = (1 * (g1 . 1)) + (1 * (g1 . 1)) by A5, A12, BINOM:13
.= ((Der1 R) . (f * g)) . i by A3, A12, BINOM:15 ;
hence ((Der1 R) . (f * g)) . i = ((df1 *' g1) + (f1 *' dg1)) . i ; :: thesis: verum

end;

suppose A14: i = 0 ; :: thesis: ((Der1 R) . (f * g)) . i = ((df1 *' g1) + (f1 *' dg1)) . i

then ((df1 *' g1) + (f1 *' dg1)) . i = (g1 . 0) + (0. R) by A1, A5, Th31
.= g1 . 0 ;
hence ((Der1 R) . (f * g)) . i = ((df1 *' g1) + (f1 *' dg1)) . i by A3, A14, BINOM:13; :: thesis: verum

end;

end;

end;

end;

end;

then (Der1 R) . (f * g) = (df1 *' g1) + (f1 *' dg1) ;
hence (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g)) by A2, POLYNOM3:def 10; :: thesis: verum