:: deftheorem Def20 defines [: ALGSTR_4:def 20 :
for X being non empty set
for M being non empty multMagma
for n, m being non zero Nat
for f being Function of (free_magma (X,n)),M
for g being Function of (free_magma (X,m)),M
for b₇ being Function of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:],M holds
( b₇ = [:f,g:] iff for x being Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:]
for y being Element of free_magma (X,n)
for z being Element of free_magma (X,m) st y = (x `1) `1 & z = (x `1) `2 holds
b₇ . x = (f . y) * (g . z) );