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 )
reconsider g = (a ") * N as Element of (G ./. N) by Th14;
assume A1: S = a * N ; :: thesis: S " = (a ") * N
A2: g * S = (@ g) * (@ S) by Def3
.= (((a ") * N) * a) * N by A1, GROUP_3:9
.= ((a ") * (N * a)) * N by GROUP_2:106
.= ((a ") * (a * N)) * N by GROUP_3:117
.= (((a ") * a) * N) * N by GROUP_2:105
.= ((1_ G) * N) * N by GROUP_1:def 5
.= (1_ G) * (N * N) by GROUP_4:45
.= (1_ G) * (carr N) by GROUP_2:76
.= carr N by GROUP_2:37 ;
A3: 1_ (G ./. N) = carr N by Th24;
S * g = (@ S) * (@ g) by Def3
.= (N * a) * ((a ") * N) by A1, GROUP_3:117
.= ((N * a) * (a ")) * N by GROUP_3:9
.= (N * (a * (a "))) * N by GROUP_2:107
.= (N * (1_ G)) * N by GROUP_1:def 5
.= (carr N) * (carr N) by GROUP_2:109
.= carr N by GROUP_2:76 ;
hence S " = (a ") * N by A2, A3, GROUP_1:def 5; :: thesis: verum