let G be Group; :: thesis: for N being normal Subgroup of G
for M being strict normal Subgroup of G
for J being strict normal Subgroup of G ./. M st J = N ./. (N,M `*` ) & M is Subgroup of N holds
(G ./. M) ./. J,G ./. N are_isomorphic
let N be normal Subgroup of G; :: thesis: for M being strict normal Subgroup of G
for J being strict normal Subgroup of G ./. M st J = N ./. (N,M `*` ) & M is Subgroup of N holds
(G ./. M) ./. J,G ./. N are_isomorphic
let M be strict normal Subgroup of G; :: thesis: for J being strict normal Subgroup of G ./. M st J = N ./. (N,M `*` ) & M is Subgroup of N holds
(G ./. M) ./. J,G ./. N are_isomorphic
let J be strict normal Subgroup of G ./. M; :: thesis: ( J = N ./. (N,M `*` ) & M is Subgroup of N implies (G ./. M) ./. J,G ./. N are_isomorphic )
assume that
A1: J = N ./. (N,M `*` ) and
A2: M is Subgroup of N ; :: thesis: (G ./. M) ./. J,G ./. N are_isomorphic
defpred S₁[ set , set ] means for a being Element of G st $1 = a * M holds
$2 = a * N;
A3: for x being Element of (G ./. M) ex y being Element of (G ./. N) st S₁[x,y]

proof

let x be Element of (G ./. M); :: thesis: ex y being Element of (G ./. N) st S₁[x,y]
consider a being Element of G such that
A4: x = a * M and
x = M * a by Th15;
reconsider y = a * N as Element of (G ./. N) by Th16;
take y ; :: thesis: S₁[x,y]
let b be Element of G; :: thesis: ( x = b * M implies y = b * N )
assume x = b * M ; :: thesis: y = b * N
then (a " ) * b in M by A4, GROUP_2:137;
then (a " ) * b in N by A2, GROUP_2:49;
hence y = b * N by GROUP_2:137; :: thesis: verum

end;

consider f being Function of (G ./. M),(G ./. N) such that
A5: for x being Element of (G ./. M) holds S₁[x,f . x] from FUNCT_2:sch 3(A3);

now

let x, y be Element of (G ./. M); :: thesis: f . (x * y) = (f . x) * (f . y)
consider a being Element of G such that
A6: x = a * M and
x = M * a by Th15;
consider b being Element of G such that
A7: y = b * M and
y = M * b by Th15;
A8: ( f . x = a * N & f . y = b * N ) by A5, A6, A7;
A9: (f . x) * (f . y) = (@ (f . x)) * (@ (f . y)) by Def4
.= ((a * N) * b) * N by A8, GROUP_3:10
.= (a * (N * b)) * N by GROUP_2:128
.= (a * (b * N)) * N by GROUP_3:140
.= a * ((b * N) * N) by GROUP_2:116
.= a * (b * N) by Th6
.= (a * b) * N by GROUP_2:127 ;
x * y = (@ x) * (@ y) by Def4
.= ((a * M) * b) * M by A6, A7, GROUP_3:10
.= (a * (M * b)) * M by GROUP_2:128
.= (a * (b * M)) * M by GROUP_3:140
.= a * ((b * M) * M) by GROUP_2:116
.= a * (b * M) by Th6
.= (a * b) * M by GROUP_2:127 ;
hence f . (x * y) = (f . x) * (f . y) by A5, A9; :: thesis: verum

end;

then reconsider f = f as Homomorphism of (G ./. M),(G ./. N) by Def7;
A10: Ker f = J

proof

let S be Element of (G ./. M); :: according to GROUP_2:def 6 :: thesis: ( ( not S in Ker f or S in J ) & ( not S in J or S in Ker f ) )
thus ( S in Ker f implies S in J ) :: thesis: ( not S in J or S in Ker f )

proof

assume S in Ker f ; :: thesis: S in J
then A11: f . S = 1_ (G ./. N) by Th50
.= carr N by Th29 ;
consider a being Element of G such that
A12: ( S = a * M & S = M * a ) by Th15;
f . S = a * N by A5, A12;
then a in N by A11, GROUP_2:136;
then reconsider q = a as Element of N by STRUCT_0:def 5;
N,M `*` = M by A2, Def1;
then ( S = q * (N,M `*` ) & S = (N,M `*` ) * q ) by A12, Th2;
hence S in J by A1, Th28; :: thesis: verum

end;

assume S in J ; :: thesis: S in Ker f
then consider a being Element of N such that
A13: ( S = a * (N,M `*` ) & S = (N,M `*` ) * a ) by A1, Th28;
reconsider a' = a as Element of G by GROUP_2:51;
N,M `*` = M by A2, Def1;
then S = a' * M by A13, Th2;
then ( f . S = a' * N & a in N ) by A5, STRUCT_0:def 5;
then f . S = carr N by GROUP_2:136
.= 1_ (G ./. N) by Th29 ;
hence S in Ker f by Th50; :: thesis: verum

end;

the carrier of (G ./. N) c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (G ./. N) or x in rng f )
assume x in the carrier of (G ./. N) ; :: thesis: x in rng f
then x in G ./. N by STRUCT_0:def 5;
then consider a being Element of G such that
A14: ( x = a * N & x = N * a ) by Th28;
reconsider S = a * M as Element of (G ./. M) by Th16;
( f . S = a * N & S in the carrier of (G ./. M) & dom f = the carrier of (G ./. M) ) by A5, FUNCT_2:def 1;
hence x in rng f by A14, FUNCT_1:def 5; :: thesis: verum

end;

then rng f = the carrier of (G ./. N) by XBOOLE_0:def 10;
then f is onto by FUNCT_2:def 3;
then Image f = G ./. N by Th67;
hence (G ./. M) ./. J,G ./. N are_isomorphic by A10, Lm3; :: thesis: verum