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