theorem :: GROUP_6:20

for G being Group
for N being normal Subgroup of G
for T1, T2 being Element of (G ./. N) holds @ (T1 * T2) = (@ T1) * (@ T2) by Def3;