let G be Group; :: thesis: for A1, A2 being Subset of G
for N being normal Subgroup of G st A1 in Cosets N & A2 in Cosets N holds
A1 * A2 in Cosets N
let A1, A2 be Subset of G; :: thesis: for N being normal Subgroup of G st A1 in Cosets N & A2 in Cosets N holds
A1 * A2 in Cosets N
let N be normal Subgroup of G; :: thesis: ( A1 in Cosets N & A2 in Cosets N implies A1 * A2 in Cosets N )
assume A1: ( A1 in Cosets N & A2 in Cosets N ) ; :: thesis: A1 * A2 in Cosets N
then consider a being Element of G such that
A2: ( A1 = a * N & A1 = N * a ) by Th15;
consider b being Element of G such that
A3: ( A2 = b * N & A2 = N * b ) by A1, Th15;
A1 * A2 = a * (N * (b * N)) by A2, A3, GROUP_3:11
.= a * ((b * N) * N) by A3, GROUP_3:15
.= a * (b * (N * N)) by GROUP_4:60
.= a * (b * N) by GROUP_2:91
.= (a * b) * N by GROUP_2:127 ;
hence A1 * A2 in Cosets N by GROUP_2:def 15; :: thesis: verum