for G being Group
for A, B being normal Subgroup of G st ( for x being Element of G ex a, b being Element of G st
( a in A & b in B & x = a * b ) ) & the carrier of A /\ the carrier of B = {(1_ G)} holds
ex h being Homomorphism of (product <*A,B*>),G st
( h is bijective & ( for a, b being Element of G st a in A & b in B holds
h . <*a,b*> = a * b ) )