for I being finite set
for G being Group
for a being b₁ -defined the carrier of b₂ -valued total Function st ( for i being object st i in I holds
a . i = 1_ G ) holds
Product a = 1_ G