let R be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for a being Element of R holds 1 '*' a = a
let a be Element of R; :: thesis: 1 '*' a = a
thus 1 '*' a = 1 * a by Def2
.= a by BINOM:13 ; :: thesis: verum