let R be non degenerated comRing; :: thesis: for D being Derivation of R holds
( D . (1. R) = 0. R & D . (0. R) = 0. R )
let D be Derivation of R; :: thesis: ( D . (1. R) = 0. R & D . (0. R) = 0. R )
A1: D . (0. R) = D . ((0. R) + (0. R))
.= (D . (0. R)) + (D . (0. R)) by Def1 ;
D . (1. R) = D . ((1. R) * (1. R))
.= ((1. R) * (D . (1. R))) + ((1. R) * (D . (1. R))) by Def1
.= (D . (1. R)) + (D . (1. R)) ;
hence ( D . (1. R) = 0. R & D . (0. R) = 0. R ) by A1, RLVECT_1:9; :: thesis: verum