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 )
assume A1: M is Subgroup of B ; :: thesis: B ./. (B,M `*` ) is Subgroup of G ./. M
set I = B ./. (B,M `*` );
set J = B,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 `*` ) & 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 & (B,M `*` ) * a = M * b ) by Th2;
hence x in the carrier of (G ./. M) by A3, Th16; :: thesis: verum

end;

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 `*` )):];
( 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):] & [:the carrier of (B ./. (B,M `*` )),the carrier of (B ./. (B,M `*` )):] c= [:the carrier of (G ./. M),the carrier of (G ./. M):] ) by A2, FUNCT_2:def 1, ZFMISC_1:119;
then A4: 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 XBOOLE_1:28;

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;
A7: ( y in the carrier of (B ./. (B,M `*` )) & z in the carrier of (B ./. (B,M `*` )) ) by A5, A6, ZFMISC_1:106;
then consider a being Element of B such that
A8: ( y = a * (B,M `*` ) & y = (B,M `*` ) * a ) by Th15;
consider b being Element of B such that
A9: ( z = b * (B,M `*` ) & z = (B,M `*` ) * b ) by A7, Th15;
reconsider W1 = y, W2 = z as Element of Cosets (B,M `*` ) by A8, A9, 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 A8, A9, 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 a' = a, b' = b as Element of G by GROUP_2:51;
A11: B,M `*` = M by A1, Def1;
then A12: ( y = a' * M & y = M * a' & z = b' * M & z = M * b' ) by A8, A9, Th2;
then reconsider V1 = y, V2 = z as Element of Cosets M by Th16;
A13: the multF of (G ./. M) . x = the multF of (G ./. M) . V1,V2 by A6
.= (a' * M) * (M * b') by A12, Def4
.= ((a' * M) * M) * b' by GROUP_3:12
.= (a' * (M * M)) * b' by GROUP_4:60
.= (a' * M) * b' by GROUP_2:91
.= a' * (M * b') by GROUP_2:128
.= a' * (b' * M) by GROUP_3:140
.= (a' * b') * M by GROUP_2:127 ;
a' * b' = a * b by GROUP_2:52;
hence the multF of (B ./. (B,M `*` )) . x = the multF of (G ./. M) . x by A10, A11, A13, Th2; :: thesis: verum

end;

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