:: deftheorem Def7 defines Zero_ C0SP1:def 7 :
for V being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V1 being Subset of V st V1 is add-closed & V1 is having-inverse & not V1 is empty holds
Zero_ (V1,V) = 0. V;