theorem Th31: :: ALGSTR_4:31

for X being set
for v, w being Element of (free_magma X) st not X is empty holds
v * w = [[[(v `1),(w `1)],(v `2)],((length v) + (length w))]