:: deftheorem defines 1_1 HILBASIS:def 3 :
for X being set
for x being Element of X
for L being non empty unital multLoopStr_0 holds 1_1 (x,L) = (0_ (X,L)) +* ((UnitBag x),(1_ L));