:: deftheorem Def19 defines canon_image ALGSTR_4:def 19 :
for X being set
for n being Nat
for b₃ being Function of (free_magma (X,n)),(free_magma X) holds
( ( n > 0 implies ( b₃ = canon_image (X,n) iff for x being set st x in dom b₃ holds
b₃ . x = [x,n] ) ) & ( not n > 0 implies ( b₃ = canon_image (X,n) iff b₃ = {} ) ) );