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