theorem Th25: :: GROUP_17:25

for q being set
for F being multMagma-Family of {q}
for G being non empty multMagma st F = q .--> G holds
for y being {b₁} -defined the carrier of b₃ -valued total Function holds
( y in the carrier of (product F) & y . q in the carrier of G & y = q .--> (y . q) )