let R be non degenerated Ring; :: thesis: for N being LeftMod of R holds the_unity_wrt the addF of N = 0. N
let N be LeftMod of R; :: thesis: the_unity_wrt the addF of N = 0. N
set F = the addF of N;
for a being Element of N holds
( the addF of N . ((0. N),a) = a & the addF of N . (a,(0. N)) = a )

proof

let a be Element of N; :: thesis: ( the addF of N . ((0. N),a) = a & the addF of N . (a,(0. N)) = a )
A1: the addF of N . ((0. N),a) = (0. N) + a
.= a ;
the addF of N . (a,(0. N)) = a + (0. N)
.= a ;
hence ( the addF of N . ((0. N),a) = a & the addF of N . (a,(0. N)) = a ) by A1; :: thesis: verum

end;

then 0. N is_a_unity_wrt the addF of N by BINOP_1:3;
hence the_unity_wrt the addF of N = 0. N by BINOP_1:def 8; :: thesis: verum