for I0, I being non empty finite set
for F0 being Group-like associative multMagma-Family of I0
for F being Group-like associative multMagma-Family of I
for H, K being Group
for q being Element of I
for G0 being Homomorphism of (product F0),H st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) & G0 is bijective holds
ex G being Homomorphism of (product F),(product <*H,K*>) st
( G is bijective & ( for x0 being Function
for k being Element of K
for h being Element of H st h = G0 . x0 & x0 in product F0 holds
G . (x0 +* (q .--> k)) = <*h,k*> ) )