:: deftheorem Def16 defines free_magma_mult ALGSTR_4:def 16 :
for X being set
for b₂ being BinOp of (free_magma_carrier X) holds
( ( not X is empty implies ( b₂ = free_magma_mult X iff for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b₂ . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) ) & ( X is empty implies ( b₂ = free_magma_mult X iff b₂ = {} ) ) );