let a, b be Element of Trivial-multLoopStr; :: thesis: a = b
thus a = {} by TARSKI:def 1
.= b by TARSKI:def 1 ; :: thesis: verum