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 that
A1: A1 in Cosets N and
A2: A2 in Cosets N ; :: thesis: A1 * A2 in Cosets N
consider a being Element of G such that
A3: A1 = a * N and
A1 = N * a by A1, Th13;
consider b being Element of G such that
A4: A2 = b * N and
A5: A2 = N * b by A2, Th13;
A1 * A2 = a * (N * (b * N)) by A3, A4, GROUP_3:10
.= a * ((b * N) * N) by A4, A5, GROUP_3:13
.= a * (b * (N * N)) by GROUP_4:45
.= a * (b * N) by GROUP_2:76
.= (a * b) * N by GROUP_2:105 ;
hence A1 * A2 in Cosets N by GROUP_2:def 15; :: thesis: verum