theorem Th3: :: GROUP_19:3

for I being set
for F being multMagma-Family of I
for a being Element of (product F) holds dom a = I