:: deftheorem Def2 defines .: MONOID_1:def 2 :
for D1, D2, D being non empty set
for f being Function of [:D1,D2:],D
for A being set
for b₆ being Function of [:(Funcs (A,D1)),(Funcs (A,D2)):],(Funcs (A,D)) holds
( b₆ = (f,D) .: A iff for f1 being Element of Funcs (A,D1)
for f2 being Element of Funcs (A,D2) holds b₆ . (f1,f2) = f .: (f1,f2) );