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
A4: ( S = a * N & S = N * a ) by GROUP_6:26;
consider b being Element of G such that
A5: ( T = b * N & T = N * b ) by GROUP_6:26;
A6: S * T = (@ S) * (@ T) by GROUP_6:24
.= (a * b) * N by A4, A5, GROUP_11:1 ;
set c = a * b;
reconsider S1 = (a * b) * N as Element of (G ./. N) by GROUP_6:27;
A7: (S * T) |^ p = ((a * b) |^ p) * N by A6, Th8
.= ((a |^ p) * (b |^ p)) * N by def3
.= ((a |^ p) * N) * ((b |^ p) * N) by GROUP_11:1 ;
A8: S |^ p = (a |^ p) * N by A4, Th8;
T |^ p = (b |^ p) * N by A5, Th8;
hence (S * T) |^ p = (S |^ p) * (T |^ p) by A7, A8, GROUP_6:def 4; :: thesis: verum