consider m being BinOp of {0}, u being Element of {0};
take multLoopStr(# {0},m,u #) ; :: thesis: multLoopStr(# {0},m,u #) is left_unital
let x be Element of multLoopStr(# {0},m,u #); :: according to VECTSP_1:def 19 :: thesis: (1. multLoopStr(# {0},m,u #)) * x = x
thus (1. multLoopStr(# {0},m,u #)) * x = 0 by TARSKI:def 1
.= x by TARSKI:def 1 ; :: thesis: verum