for G being commutative Group
for I0, I being non empty finite set
for q being Element of I
for x being b₃ -defined the carrier of b₁ -valued total Function
for x0 being b₂ -defined the carrier of b₁ -valued total Function
for k being Element of G st not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k) holds
Product x = (Product x0) * k