:: deftheorem Def18 defines length ALGSTR_4:def 18 :
for X being set
for w being Element of (free_magma X) holds
( ( not X is empty implies length w = w `2 ) & ( X is empty implies length w = 0 ) );