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:90;
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:78;
then A5: N = (B "\/" N),N `*` by Def1;
A6: B is Subgroup of B "\/" N by GROUP_4:78;
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, A1, A7, XBOOLE_1:28;
reconsider x9 = x as Element of G by GROUP_2:51;
reconsider x99 = x as Element of (B "\/" N) by A6, GROUP_2:51;
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:70
.= x9 * N by Def9 ;
then ((nat_hom N) | the carrier of B) . x = N * x9 by GROUP_3:140;
then y in (B "\/" N) ./. ((B "\/" N),N `*` ) by A8, A10, A9, 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;
A11: (B "\/" N) ./. ((B "\/" N),N `*` ) is Subgroup of G ./. N by A4, Th34;

now

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:51;
A12: ( (nat_hom N) . a9 = g . a & (nat_hom N) . b9 = g . b ) by FUNCT_1:72;
a * b = a9 * b9 by GROUP_2:52;
hence g . (a * b) = (nat_hom N) . (a9 * b9) by FUNCT_1:72
.= ((nat_hom N) . a9) * ((nat_hom N) . b9) by Def7
.= (g . a) * (g . b) by A11, A12, GROUP_2:52 ;
:: thesis: verum

end;

then reconsider g = g as Homomorphism of B,((B "\/" N) ./. ((B "\/" N),N `*` )) by Def7;
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:51;
A14: 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 A14, 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 A14, 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
A15: x = b * ((B "\/" N),N `*` ) and
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
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, STRUCT_0:def 5;
x = (a1 * a2) * N by A5, A15, A16, Th2
.= a1 * (a2 * N) by GROUP_2:127
.= a1 * N by A18, GROUP_2:136
.= (nat_hom N) . a1 by Def9
.= g . a1 by A19, FUNCT_1:72 ;
hence x in rng g by A3, A19, 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 A13, Lm3; :: thesis: verum