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