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 object ; :: 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 Th13;
reconsider b = a as Element of G by GROUP_2:42;
(B,M) `*` = M by A1, Def1;
then a * ((B,M) `*`) = b * M by Th2;
hence x in the carrier of (G ./. M) by A3, Th14; :: thesis: verum

end;

A4: now :: thesis: for x being object st x in dom the multF of (B ./. ((B,M) `*`)) holds
the multF of (B ./. ((B,M) `*`)) . x = the multF of (G ./. M) . x

let x be object ; :: 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 object such that
A6: [y,z] = x by RELAT_1:def 1;
z in the carrier of (B ./. ((B,M) `*`)) by A5, A6, ZFMISC_1:87;
then consider b being Element of B such that
A7: z = b * ((B,M) `*`) and
A8: z = ((B,M) `*`) * b by Th13;
y in the carrier of (B ./. ((B,M) `*`)) by A5, A6, ZFMISC_1:87;
then consider a being Element of B such that
A9: y = a * ((B,M) `*`) and
y = ((B,M) `*`) * a by Th13;
reconsider W1 = y, W2 = z as Element of Cosets ((B,M) `*`) by A9, A7, Th14;
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, Def3
.= ((a * ((B,M) `*`)) * ((B,M) `*`)) * b by GROUP_3:11
.= (a * (((B,M) `*`) * ((B,M) `*`))) * b by GROUP_4:45
.= (a * ((B,M) `*`)) * b by GROUP_2:76
.= a * (((B,M) `*`) * b) by GROUP_2:106
.= a * (b * ((B,M) `*`)) by GROUP_3:117
.= (a * b) * ((B,M) `*`) by GROUP_2:105 ;
reconsider a9 = a, b9 = b as Element of G by GROUP_2:42;
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, Th14;
A13: a9 * b9 = a * b by GROUP_2:43;
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, Def3
.= ((a9 * M) * M) * b9 by GROUP_3:11
.= (a9 * (M * M)) * b9 by GROUP_4:45
.= (a9 * M) * b9 by GROUP_2:76
.= a9 * (M * b9) by GROUP_2:106
.= a9 * (b9 * M) by GROUP_3:117
.= (a9 * b9) * M by GROUP_2:105 ;
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:96;
then the multF of (B ./. ((B,M) `*`)) = the multF of (G ./. M) || the carrier of (B ./. ((B,M) `*`)) by A4, FUNCT_1:46;
hence B ./. ((B,M) `*`) is Subgroup of G ./. M by A2, GROUP_2:def 5; :: thesis: verum