let S, T be Element of (G ./. N); :: according to GROUPP_1:def 3 :: thesis: (S * T) |^ p = (S |^ p) * (T |^ p)
consider a being Element of G such that
A1: ( S = a * N & S = N * a ) by GROUP_6:21;
consider b being Element of G such that
A2: ( T = b * N & T = N * b ) by GROUP_6:21;
A3: S * T = (@ S) * (@ T) by GROUP_6:19
.= (a * b) * N by A1, A2, GROUP_11:1 ;
set c = a * b;
A4: (S * T) |^ p = ((a * b) |^ p) * N by A3, Th8
.= ((a |^ p) * (b |^ p)) * N by Def3
.= ((a |^ p) * N) * ((b |^ p) * N) by GROUP_11:1 ;
A5: S |^ p = (a |^ p) * N by A1, Th8;
T |^ p = (b |^ p) * N by A2, Th8;
hence (S * T) |^ p = (S |^ p) * (T |^ p) by A4, A5, GROUP_6:def 3; :: thesis: verum