theorem :: ALGSTR_4:33

for X being set
for v, w being Element of (free_magma X) holds length (v * w) = (length v) + (length w)