theorem Th29: :: GROUP_17:29

for I being non empty finite set
for F being Group-like associative multMagma-Family of I
for x being b₁ -defined total Function st ( for p being Element of I holds x . p in F . p ) holds
x in the carrier of (product F)