theorem Th19: :: GROUP_23:24

for G being Group
for H being Subgroup of G holds
( incl (H,G) is one-to-one & Image (incl (H,G)) = multMagma(# the carrier of H, the multF of H #) )