let G be Group; :: thesis: for B being Subgroup of G
for N being strict normal Subgroup of G holds (B "\/" N) ./. (((B "\/" N),N) `*`),B ./. (B /\ N) are_isomorphic
let B be Subgroup of G; :: thesis: for N being strict normal Subgroup of G holds (B "\/" N) ./. (((B "\/" N),N) `*`),B ./. (B /\ N) are_isomorphic
let N be strict normal Subgroup of G; :: thesis: (B "\/" N) ./. (((B "\/" N),N) `*`),B ./. (B /\ N) are_isomorphic
set f = nat_hom N;
set g = (nat_hom N) | the carrier of B;
set I = (B "\/" N) ./. (((B "\/" N),N) `*`);
set J = ((B "\/" N),N) `*` ;
A1: the carrier of B c= the carrier of G by GROUP_2:def 5;
A2: ( dom ((nat_hom N) | the carrier of B) = (dom (nat_hom N)) /\ the carrier of B & dom (nat_hom N) = the carrier of G ) by FUNCT_2:def 1, RELAT_1:61;
then A3: dom ((nat_hom N) | the carrier of B) = the carrier of B by A1, XBOOLE_1:28;
A4: N is Subgroup of B "\/" N by GROUP_4:60;
then A5: N = ((B "\/" N),N) `*` by Def1;
A6: B is Subgroup of B "\/" N by GROUP_4:60;
rng ((nat_hom N) | the carrier of B) c= the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((nat_hom N) | the carrier of B) or y in the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) )
assume y in rng ((nat_hom N) | the carrier of B) ; :: thesis: y in the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`))
then consider x being object such that
A7: x in dom ((nat_hom N) | the carrier of B) and
A8: ((nat_hom N) | the carrier of B) . x = y by FUNCT_1:def 3;
reconsider x = x as Element of B by A2, A1, A7, XBOOLE_1:28;
reconsider x9 = x as Element of G by GROUP_2:42;
reconsider x99 = x as Element of (B "\/" N) by A6, GROUP_2:42;
A9: ( x99 * (((B "\/" N),N) `*`) = x9 * N & N * x9 = (((B "\/" N),N) `*`) * x99 ) by A5, Th2;
A10: ((nat_hom N) | the carrier of B) . x = (nat_hom N) . x9 by A7, FUNCT_1:47
.= x9 * N by Def8 ;
then ((nat_hom N) | the carrier of B) . x = N * x9 by GROUP_3:117;
then y in (B "\/" N) ./. (((B "\/" N),N) `*`) by A8, A10, A9, Th23;
hence y in the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) ; :: thesis: verum

end;

then reconsider g = (nat_hom N) | the carrier of B as Function of B,((B "\/" N) ./. (((B "\/" N),N) `*`)) by A3, FUNCT_2:def 1, RELSET_1:4;
A11: (B "\/" N) ./. (((B "\/" N),N) `*`) is Subgroup of G ./. N by A4, Th28;

now :: thesis: for a, b being Element of B holds g . (a * b) = (g . a) * (g . b)

let a, b be Element of B; :: thesis: g . (a * b) = (g . a) * (g . b)
reconsider a9 = a, b9 = b as Element of G by GROUP_2:42;
A12: ( (nat_hom N) . a9 = g . a & (nat_hom N) . b9 = g . b ) by FUNCT_1:49;
a * b = a9 * b9 by GROUP_2:43;
hence g . (a * b) = (nat_hom N) . (a9 * b9) by FUNCT_1:49
.= ((nat_hom N) . a9) * ((nat_hom N) . b9) by Def6
.= (g . a) * (g . b) by A11, A12, GROUP_2:43 ;
:: thesis: verum

end;

then reconsider g = g as Homomorphism of B,((B "\/" N) ./. (((B "\/" N),N) `*`)) by Def6;
A13: Ker g = B /\ N

proof

let b be Element of B; :: according to GROUP_2:def 6 :: thesis: ( ( not b in Ker g or b in B /\ N ) & ( not b in B /\ N or b in Ker g ) )
reconsider c = b as Element of G by GROUP_2:42;
A14: g . b = (nat_hom N) . c by FUNCT_1:49
.= c * N by Def8 ;
thus ( b in Ker g implies b in B /\ N ) :: thesis: ( not b in B /\ N or b in Ker g )

proof

assume b in Ker g ; :: thesis: b in B /\ N
then g . b = 1_ ((B "\/" N) ./. (((B "\/" N),N) `*`)) by Th41
.= carr (((B "\/" N),N) `*`) by Th24
.= carr N by A4, Def1 ;
then ( b in B & b in N ) by A14, GROUP_2:113;
hence b in B /\ N by GROUP_2:82; :: thesis: verum

end;

assume b in B /\ N ; :: thesis: b in Ker g
then b in N by GROUP_2:82;
then c * N = carr (((B "\/" N),N) `*`) by A5, GROUP_2:113
.= 1_ ((B "\/" N) ./. (((B "\/" N),N) `*`)) by Th24 ;
hence b in Ker g by A14, Th41; :: thesis: verum

end;

the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) c= rng g

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) or x in rng g )
assume x in the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) ; :: thesis: x in rng g
then x in (B "\/" N) ./. (((B "\/" N),N) `*`) ;
then consider b being Element of (B "\/" N) such that
A15: x = b * (((B "\/" N),N) `*`) and
x = (((B "\/" N),N) `*`) * b by Th23;
( B * N = N * B & b in B "\/" N ) by GROUP_5:8;
then consider a1, a2 being Element of G such that
A16: b = a1 * a2 and
A17: a1 in B and
A18: a2 in N by GROUP_5:5;
A19: a1 in the carrier of B by A17;
x = (a1 * a2) * N by A5, A15, A16, Th2
.= a1 * (a2 * N) by GROUP_2:105
.= a1 * N by A18, GROUP_2:113
.= (nat_hom N) . a1 by Def8
.= g . a1 by A19, FUNCT_1:49 ;
hence x in rng g by A3, A19, FUNCT_1:def 3; :: thesis: verum

end;

then the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) = rng g ;
then g is onto ;
then Image g = (B "\/" N) ./. (((B "\/" N),N) `*`) by Th57;
hence (B "\/" N) ./. (((B "\/" N),N) `*`),B ./. (B /\ N) are_isomorphic by A13, Lm3; :: thesis: verum