:: deftheorem Def5 defines addFinS MATRIX11:def 5 :
for K being non empty addLoopStr
for b₂ being BinOp of ( the carrier of K *) holds
( b₂ = addFinS K iff for p1, p2 being Element of the carrier of K * holds b₂ . (p1,p2) = p1 + p2 );