let R be domRing; :: thesis: for f, g being Element of the carrier of (Polynom-Ring R) 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: (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g))

per cases ( not f is constant or f is constant ) ;

suppose not f is constant ; :: thesis: (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g))

hence (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g)) by Th35; :: thesis: verum

end;

suppose f is constant ; :: thesis: (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g))

hence (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g)) by Th34; :: thesis: verum

end;

end;