let G be Group; :: thesis: for a being Element of G
for N being normal Subgroup of G holds
( a * N in Cosets N & N * a in Cosets N )
let a be Element of G; :: thesis: for N being normal Subgroup of G holds
( a * N in Cosets N & N * a in Cosets N )
let N be normal Subgroup of G; :: thesis: ( a * N in Cosets N & N * a in Cosets N )
N * a in Right_Cosets N by GROUP_2:def 16;
hence ( a * N in Cosets N & N * a in Cosets N ) by GROUP_2:def 15, GROUP_3:127; :: thesis: verum