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;