let K be non empty left_zeroed right_zeroed addLoopStr ; :: thesis: 0. K is_a_unity_wrt the addF of K
now :: thesis: for a being Element of K holds
( the addF of K . ((0. K),a) = a & the addF of K . (a,(0. K)) = a )
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 2 ; :: 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 4 ; :: thesis: verum
end;
hence 0. K is_a_unity_wrt the addF of K by BINOP_1:3; :: thesis: verum