let R be domRing; :: thesis: for k being Nat
for f being Element of the carrier of (Polynom-Ring R) holds ((Der1 R) |^ 0) . (f |^ k) = f |^ k
let k be Nat; :: thesis: for f being Element of the carrier of (Polynom-Ring R) holds ((Der1 R) |^ 0) . (f |^ k) = f |^ k
let f be Element of the carrier of (Polynom-Ring R); :: thesis: ((Der1 R) |^ 0) . (f |^ k) = f |^ k
(Der1 R) |^ 0 = id (Polynom-Ring R) by VECTSP11:18;
hence ((Der1 R) |^ 0) . (f |^ k) = f |^ k ; :: thesis: verum