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