let K be non empty left_zeroed right_zeroed addLoopStr ; :: thesis: 0. K is_a_unity_wrt the addF of K

now

let a be Element of K; :: thesis: ( the addF of K . (0. K),a = a & the addF of K . a,(0. K) = a )
thus the addF of K . (0. K),a = (0. K) + a
.= a by ALGSTR_1:def 5 ; :: thesis: the addF of K . a,(0. K) = a
thus the addF of K . a,(0. K) = a + (0. K)
.= a by RLVECT_1:def 7 ; :: thesis: verum

end;

hence 0. K is_a_unity_wrt the addF of K by BINOP_1:11; :: thesis: verum