for G1, G2 being Group
for H1, H2 being Subgroup of G1
for f being Function of the carrier of G1, the carrier of G2
for A being Subset of G1 st A = the carrier of H1 \/ the carrier of H2 holds
f .: the carrier of (H1 "\/" H2) = f .: the carrier of (gr A) by Th4;