let R be non empty right_zeroed addLoopStr ; :: thesis: for a being Element of R holds 1 * a = a
let a be Element of R; :: thesis: 1 * a = a
thus 1 * a = (Nat-mult-left R) . ((0 + 1),a)
.= a + ((Nat-mult-left R) . (0,a)) by Def3
.= a + (0. R) by Def3
.= a by RLVECT_1:def 4 ; :: thesis: verum