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: B is Subgroup of B "\/" N by GROUP_4:78;
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 & the carrier of B c= the carrier of G ) by FUNCT_2:def 1, GROUP_2:def 5, RELAT_1:90;
then A3: dom ((nat_hom N) | the carrier of B) = the carrier of B by XBOOLE_1:28;
A4: N is Subgroup of B "\/" N by GROUP_4:78;
then A5: N = (B "\/" N),N `*` by Def1;
A6: (B "\/" N) ./. ((B "\/" N),N `*` ) is Subgroup of G ./. N by A4, Th34;
rng ((nat_hom N) | the carrier of B) c= the carrier of ((B "\/" N) ./. ((B "\/" N),N `*` ))

proof

let y be set ; :: 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 set 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 5;
reconsider x = x as Element of B by A2, A7, XBOOLE_1:28;
reconsider x'' = x as Element of (B "\/" N) by A1, GROUP_2:51;
reconsider x' = x as Element of G by GROUP_2:51;
A9: ((nat_hom N) | the carrier of B) . x = (nat_hom N) . x' by A7, FUNCT_1:70
.= x' * N by Def9 ;
then A10: ((nat_hom N) | the carrier of B) . x = N * x' by GROUP_3:140;
( x'' * ((B "\/" N),N `*` ) = x' * N & N * x' = ((B "\/" N),N `*` ) * x'' ) by A5, Th2;
then y in (B "\/" N) ./. ((B "\/" N),N `*` ) by A8, A9, A10, Th28;
hence y in the carrier of ((B "\/" N) ./. ((B "\/" N),N `*` )) by STRUCT_0:def 5; :: 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:11;

now

let a, b be Element of B; :: thesis: g . (a * b) = (g . a) * (g . b)
reconsider a' = a, b' = b as Element of G by GROUP_2:51;
A11: ( (nat_hom N) . a' = g . a & (nat_hom N) . b' = g . b ) by FUNCT_1:72;
( a * b in the carrier of B & a * b = a' * b' & a' * b' in the carrier of G ) by GROUP_2:52;
hence g . (a * b) = (nat_hom N) . (a' * b') by FUNCT_1:72
.= ((nat_hom N) . a') * ((nat_hom N) . b') by Def7
.= (g . a) * (g . b) by A6, A11, GROUP_2:52 ;
:: thesis: verum

end;

then reconsider g = g as Homomorphism of B,((B "\/" N) ./. ((B "\/" N),N `*` )) by Def7;
A12: 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:51;
A13: g . b = (nat_hom N) . c by FUNCT_1:72
.= c * N by Def9 ;
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 Th50
.= carr ((B "\/" N),N `*` ) by Th29
.= carr N by A4, Def1 ;
then ( b in B & b in N ) by A13, GROUP_2:136, STRUCT_0:def 5;
hence b in B /\ N by GROUP_2:99; :: thesis: verum

end;

assume b in B /\ N ; :: thesis: b in Ker g
then b in N by GROUP_2:99;
then c * N = carr ((B "\/" N),N `*` ) by A5, GROUP_2:136
.= 1_ ((B "\/" N) ./. ((B "\/" N),N `*` )) by Th29 ;
hence b in Ker g by A13, Th50; :: thesis: verum

end;

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

proof

let x be set ; :: 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 `*` ) by STRUCT_0:def 5;
then consider b being Element of (B "\/" N) such that
A14: ( x = b * ((B "\/" N),N `*` ) & x = ((B "\/" N),N `*` ) * b ) by Th28;
( B * N = N * B & b in B "\/" N ) by GROUP_5:8, STRUCT_0:def 5;
then consider a1, a2 being Element of G such that
A15: b = a1 * a2 and
A16: ( a1 in B & a2 in N ) by GROUP_5:5;
A17: ( a1 in the carrier of B & a1 in the carrier of G ) by A16, STRUCT_0:def 5;
x = (a1 * a2) * N by A5, A14, A15, Th2
.= a1 * (a2 * N) by GROUP_2:127
.= a1 * N by A16, GROUP_2:136
.= (nat_hom N) . a1 by Def9
.= g . a1 by A17, FUNCT_1:72 ;
hence x in rng g by A3, A17, FUNCT_1:def 5; :: thesis: verum

end;

then the carrier of ((B "\/" N) ./. ((B "\/" N),N `*` )) = rng g by XBOOLE_0:def 10;
then g is onto by FUNCT_2:def 3;
then Image g = (B "\/" N) ./. ((B "\/" N),N `*` ) by Th67;
hence (B "\/" N) ./. ((B "\/" N),N `*` ),B ./. (B /\ N) are_isomorphic by A12, Lm3; :: thesis: verum