theorem Th40: :: GROUP_19:40
for I being non empty set
for F, G being Group-Family of I
for h being non empty Function st I = dom h & ( for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & hi is bijective ) ) holds
ProductMap (F,G,h) is bijective