:: deftheorem Def26 defines OSFreeGen OSAFREE:def 26 :
for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for b₃ being OSGeneratorSet of FreeOSA X holds
( b₃ = OSFreeGen X iff for s being Element of S holds b₃ . s = OSFreeGen (s,X) );