theorem Th9: :: GROUP_17:9

for G being non empty multMagma
for q being set
for z being Element of G
for f being {b₂} -defined the carrier of b₁ -valued total Function st f = q .--> z holds
Product f = z