:: deftheorem Def2 defines dilation MORPH_01:def 2 :
for E being RealLinearSpace
for B being binary-image of E
for b₃ being Function of (bool the carrier of E),(bool the carrier of E) holds
( b₃ = dilation B iff for A being binary-image of E holds b₃ . A = A (+) B );