let L be domRing; :: thesis: for y being Element of the carrier of L
for D being Derivation of L holds (D |^ 1) . y = D . y
let y be Element of the carrier of L; :: thesis: for D being Derivation of L holds (D |^ 1) . y = D . y
let D be Derivation of L; :: thesis: (D |^ 1) . y = D . y
A1: D |^ 0 = id L by VECTSP11:18;
(D |^ 1) . y = (D |^ (0 + 1)) . y
.= D . ((D |^ 0) . y) by RINGDER1:9
.= D . y by A1 ;
hence (D |^ 1) . y = D . y ; :: thesis: verum