theorem :: GROUP_12:13

for n being non zero Nat
for G, F being Group-like associative commutative multMagma-Family of Seg n st ( for k being Element of Seg n holds F . k = ProjGroup (G,k) ) holds
ex f being Homomorphism of (product F),(product G) st
( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product G) st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )