let G be Group; :: thesis: for B being Subgroup of G
for M being strict normal Subgroup of G st M is Subgroup of B holds
B ./. (B,M `*` ) is Subgroup of G ./. M
let B be Subgroup of G; :: thesis: for M being strict normal Subgroup of G st M is Subgroup of B holds
B ./. (B,M `*` ) is Subgroup of G ./. M
let M be strict normal Subgroup of G; :: thesis: ( M is Subgroup of B implies B ./. (B,M `*` ) is Subgroup of G ./. M )
set I = B ./. (B,M `*` );
set J = B,M `*` ;
set g = the multF of (B ./. (B,M `*` ));
set f = the multF of (G ./. M);
set X = [:the carrier of (B ./. (B,M `*` )),the carrier of (B ./. (B,M `*` )):];
assume A1: M is Subgroup of B ; :: thesis: B ./. (B,M `*` ) is Subgroup of G ./. M
A2: the carrier of (B ./. (B,M `*` )) c= the carrier of (G ./. M)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (B ./. (B,M `*` )) or x in the carrier of (G ./. M) )
assume x in the carrier of (B ./. (B,M `*` )) ; :: thesis: x in the carrier of (G ./. M)
then consider a being Element of B such that
A3: x = a * (B,M `*` ) and
x = (B,M `*` ) * a by Th15;
reconsider b = a as Element of G by GROUP_2:51;
B,M `*` = M by A1, Def1;
then a * (B,M `*` ) = b * M by Th2;
hence x in the carrier of (G ./. M) by A3, Th16; :: thesis: verum

end;

A4: now

let x be set ; :: thesis: ( x in dom the multF of (B ./. (B,M `*` )) implies the multF of (B ./. (B,M `*` )) . x = the multF of (G ./. M) . x )
assume A5: x in dom the multF of (B ./. (B,M `*` )) ; :: thesis: the multF of (B ./. (B,M `*` )) . x = the multF of (G ./. M) . x
then consider y, z being set such that
A6: [y,z] = x by RELAT_1:def 1;
z in the carrier of (B ./. (B,M `*` )) by A5, A6, ZFMISC_1:106;
then consider b being Element of B such that
A7: z = b * (B,M `*` ) and
A8: z = (B,M `*` ) * b by Th15;
y in the carrier of (B ./. (B,M `*` )) by A5, A6, ZFMISC_1:106;
then consider a being Element of B such that
A9: y = a * (B,M `*` ) and
y = (B,M `*` ) * a by Th15;
reconsider W1 = y, W2 = z as Element of Cosets (B,M `*` ) by A9, A7, Th16;
A10: the multF of (B ./. (B,M `*` )) . x = the multF of (B ./. (B,M `*` )) . W1,W2 by A6
.= (a * (B,M `*` )) * ((B,M `*` ) * b) by A9, A8, Def4
.= ((a * (B,M `*` )) * (B,M `*` )) * b by GROUP_3:12
.= (a * ((B,M `*` ) * (B,M `*` ))) * b by GROUP_4:60
.= (a * (B,M `*` )) * b by GROUP_2:91
.= a * ((B,M `*` ) * b) by GROUP_2:128
.= a * (b * (B,M `*` )) by GROUP_3:140
.= (a * b) * (B,M `*` ) by GROUP_2:127 ;
reconsider a9 = a, b9 = b as Element of G by GROUP_2:51;
A11: B,M `*` = M by A1, Def1;
then A12: y = a9 * M by A9, Th2;
z = b9 * M by A7, A11, Th2;
then reconsider V1 = y, V2 = z as Element of Cosets M by A12, Th16;
A13: a9 * b9 = a * b by GROUP_2:52;
A14: z = M * b9 by A8, A11, Th2;
the multF of (G ./. M) . x = the multF of (G ./. M) . V1,V2 by A6
.= (a9 * M) * (M * b9) by A12, A14, Def4
.= ((a9 * M) * M) * b9 by GROUP_3:12
.= (a9 * (M * M)) * b9 by GROUP_4:60
.= (a9 * M) * b9 by GROUP_2:91
.= a9 * (M * b9) by GROUP_2:128
.= a9 * (b9 * M) by GROUP_3:140
.= (a9 * b9) * M by GROUP_2:127 ;
hence the multF of (B ./. (B,M `*` )) . x = the multF of (G ./. M) . x by A10, A11, A13, Th2; :: thesis: verum

end;

( dom the multF of (B ./. (B,M `*` )) = [:the carrier of (B ./. (B,M `*` )),the carrier of (B ./. (B,M `*` )):] & dom the multF of (G ./. M) = [:the carrier of (G ./. M),the carrier of (G ./. M):] ) by FUNCT_2:def 1;
then dom the multF of (B ./. (B,M `*` )) = (dom the multF of (G ./. M)) /\ [:the carrier of (B ./. (B,M `*` )),the carrier of (B ./. (B,M `*` )):] by A2, XBOOLE_1:28, ZFMISC_1:119;
then the multF of (B ./. (B,M `*` )) = the multF of (G ./. M) || the carrier of (B ./. (B,M `*` )) by A4, FUNCT_1:68;
hence B ./. (B,M `*` ) is Subgroup of G ./. M by A2, GROUP_2:def 5; :: thesis: verum