for I being non empty finite set
for G being Group
for H being Subgroup of G
for x being b₁ -defined the carrier of b₂ -valued total Function
for x0 being b₁ -defined the carrier of b₃ -valued total Function st x = x0 holds
Product x = Product x0