:: deftheorem Def8 defines .:^2 MONOID_1:def 8 :
for D1, D2, D being non empty set
for f being Function of [:D1,D2:],D
for b₅ being Function of [:(bool D1),(bool D2):],(bool D) holds
( b₅ = f .:^2 iff for x being Element of [:(bool D1),(bool D2):] holds b₅ . x = f .: [:(x `1),(x `2):] );