let R be non empty left_zeroed addLoopStr ; :: thesis: for a being Element of R holds a * 1 = a
let a be Element of R; :: thesis: a * 1 = a
thus a * 1 = (Nat-mult-right R) . (a,(0 + 1))
.= ((Nat-mult-right R) . (a,0)) + a by Def7
.= (0. R) + a by Def7
.= a by ALGSTR_1:def 5 ; :: thesis: verum