let G be Group; :: thesis: for a being Element of G
for N being normal Subgroup of G
for S being Element of (G ./. N) st S = a * N holds
S " = (a " ) * N
let a be Element of G; :: thesis: for N being normal Subgroup of G
for S being Element of (G ./. N) st S = a * N holds
S " = (a " ) * N
let N be normal Subgroup of G; :: thesis: for S being Element of (G ./. N) st S = a * N holds
S " = (a " ) * N
let S be Element of (G ./. N); :: thesis: ( S = a * N implies S " = (a " ) * N )
assume A1: S = a * N ; :: thesis: S " = (a " ) * N
reconsider g = (a " ) * N as Element of (G ./. N) by Th16;
A2: S * g = (@ S) * (@ g) by Def4
.= (N * a) * ((a " ) * N) by A1, GROUP_3:140
.= ((N * a) * (a " )) * N by GROUP_3:10
.= (N * (a * (a " ))) * N by GROUP_2:129
.= (N * (1_ G)) * N by GROUP_1:def 6
.= (carr N) * (carr N) by GROUP_2:132
.= carr N by GROUP_2:91 ;
A3: g * S = (@ g) * (@ S) by Def4
.= (((a " ) * N) * a) * N by A1, GROUP_3:10
.= ((a " ) * (N * a)) * N by GROUP_2:128
.= ((a " ) * (a * N)) * N by GROUP_3:140
.= (((a " ) * a) * N) * N by GROUP_2:127
.= ((1_ G) * N) * N by GROUP_1:def 6
.= (1_ G) * (N * N) by GROUP_4:60
.= (1_ G) * (carr N) by GROUP_2:91
.= carr N by GROUP_2:43 ;
1_ (G ./. N) = carr N by Th29;
hence S " = (a " ) * N by A2, A3, GROUP_1:def 6; :: thesis: verum