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 Th13;
reconsider y = a * N as Element of (G ./. N) by Th14;
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:114;
then (a ") * b in N by A2, GROUP_2:40;
hence y = b * N by GROUP_2:114; :: 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 :: thesis: for x, y being Element of (G ./. M) holds f . (x * y) = (f . x) * (f . y)

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 Th13;
consider b being Element of G such that
A7: y = b * M and
y = M * b by Th13;
A8: x * y = (@ x) * (@ y) by Def3
.= ((a * M) * b) * M by A6, A7, GROUP_3:9
.= (a * (M * b)) * M by GROUP_2:106
.= (a * (b * M)) * M by GROUP_3:117
.= a * ((b * M) * M) by GROUP_2:96
.= a * (b * M) by Th5
.= (a * b) * M by GROUP_2:105 ;
A9: f . y = b * N by A5, A7;
A10: f . x = a * N by A5, A6;
(f . x) * (f . y) = (@ (f . x)) * (@ (f . y)) by Def3
.= ((a * N) * b) * N by A10, A9, GROUP_3:9
.= (a * (N * b)) * N by GROUP_2:106
.= (a * (b * N)) * N by GROUP_3:117
.= a * ((b * N) * N) by GROUP_2:96
.= a * (b * N) by Th5
.= (a * b) * N by GROUP_2:105 ;
hence f . (x * y) = (f . x) * (f . y) by A5, A8; :: thesis: verum

end;

then reconsider f = f as Homomorphism of (G ./. M),(G ./. N) by Def6;
A11: 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 A12: f . S = 1_ (G ./. N) by Th41
.= carr N by Th24 ;
consider a being Element of G such that
A13: S = a * M and
A14: S = M * a by Th13;
f . S = a * N by A5, A13;
then a in N by A12, GROUP_2:113;
then reconsider q = a as Element of N ;
(N,M) `*` = M by A2, Def1;
then ( S = q * ((N,M) `*`) & S = ((N,M) `*`) * q ) by A13, A14, Th2;
hence S in J by A1, Th23; :: thesis: verum

end;

assume S in J ; :: thesis: S in Ker f
then consider a being Element of N such that
A15: S = a * ((N,M) `*`) and
S = ((N,M) `*`) * a by A1, Th23;
reconsider a9 = a as Element of G by GROUP_2:42;
(N,M) `*` = M by A2, Def1;
then S = a9 * M by A15, Th2;
then A16: f . S = a9 * N by A5;
a in N ;
then f . S = carr N by A16, GROUP_2:113
.= 1_ (G ./. N) by Th24 ;
hence S in Ker f by Th41; :: thesis: verum

end;

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

proof

let x be object ; :: 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 ;
then consider a being Element of G such that
A17: x = a * N and
x = N * a by Th23;
reconsider S = a * M as Element of (G ./. M) by Th14;
( f . S = a * N & dom f = the carrier of (G ./. M) ) by A5, FUNCT_2:def 1;
hence x in rng f by A17, FUNCT_1:def 3; :: thesis: verum

end;

then rng f = the carrier of (G ./. N) ;
then f is onto ;
then Image f = G ./. N by Th57;
hence (G ./. M) ./. J,G ./. N are_isomorphic by A11, Lm3; :: thesis: verum