:: Homomorphisms and Isomorphisms of Groups. Quotient Group
:: by Wojciech A. Trybulec and Micha{\l} J. Trybulec
::
:: Received October 3, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

theorem Th1: :: GROUP_6:1
for A, B being non empty set
for f being Function of A,B holds
( f is one-to-one iff for a, b being Element of A st f . a = f . b holds
a = b )
proofend;

definition
let G be Group;
let A be Subgroup of G;
:: original:Subgroup
redefine mode Subgroup of A ->  Subgroup of G;
coherence
 for b1 being Subgroup of A holds b1 is Subgroup of G by GROUP_2:56;
end;

registration
let G be Group;
cluster (1). G ->  normal ;
coherence
 (1). G is normal by GROUP_3:114;
cluster (Omega). G ->  normal ;
coherence
 (Omega). G is normal by GROUP_3:114;
end;

theorem Th2: :: GROUP_6:2
for G being Group
for A being Subgroup of G
for a being Element of G
for X being Subgroup of A
for x being Element of A st x = a holds
( x * X = a * X & X * x = X * a )
proofend;

theorem :: GROUP_6:3
for G being Group
for A being Subgroup of G
for X, Y being Subgroup of A holds X /\ Y = X /\ Y
proofend;

theorem Th4: :: GROUP_6:4
for G being Group
for a, b being Element of G holds
( (a * b) * (a ") = b |^ (a ") & a * (b * (a ")) = b |^ (a ") )
proofend;

theorem Th5: :: GROUP_6:5
for G being Group
for A being Subgroup of G
for a being Element of G holds
( (a * A) * A = a * A & a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a )
proofend;

theorem Th6: :: GROUP_6:6
for G being Group
for A1 being Subset of G st A1 =  {  [.a,b.] where a, b is Element of G : verum  }  holds
G ` = gr A1
proofend;

theorem Th7: :: GROUP_6:7
for G being strict Group
for B being strict Subgroup of G holds
( G ` is Subgroup of B iff for a, b being Element of G holds [.a,b.] in B )
proofend;

theorem Th8: :: GROUP_6:8
for G being Group
for B being Subgroup of G
for N being normal Subgroup of G st N is Subgroup of B holds
N is normal Subgroup of B
proofend;

definition
let G be Group;
let B be Subgroup of G;
let M be normal Subgroup of G;
assume A1: multMagma(# the carrier of M, the multF of M #) is Subgroup of B ;
func(B,M) `*`  ->  strict normal Subgroup of B equals :Def1: :: GROUP_6:def 1
 multMagma(# the carrier of M, the multF of M #);
coherence
 multMagma(# the carrier of M, the multF of M #) is strict normal Subgroup of B
proofend;
correctness
;
end;

:: deftheorem Def1 defines `*` GROUP_6:def_1_:_
 for G being Group
for B being Subgroup of G
for M being normal Subgroup of G st multMagma(# the carrier of M, the multF of M #) is Subgroup of B holds
(B,M) `*` = multMagma(# the carrier of M, the multF of M #);

theorem Th9: :: GROUP_6:9
for G being Group
for B being Subgroup of G
for N being normal Subgroup of G holds
( B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B )
proofend;

definition
let G be Group;
let B be Subgroup of G;
let N be normal Subgroup of G;
:: original:/\
redefine funcB /\ N ->  strict normal Subgroup of B;
coherence
 B /\ N is strict normal Subgroup of B by Th9;
end;

definition
let G be Group;
let N be normal Subgroup of G;
let B be Subgroup of G;
:: original:/\
redefine funcN /\ B ->  strict normal Subgroup of B;
coherence
 N /\ B is strict normal Subgroup of B by Th9;
end;

definition
let G be non empty 1-sorted ;
redefine attr G is trivial  means :Def2: :: GROUP_6:def 2
 ex x being set st the carrier of G = {x};
compatibility
 ( G is trivial iff ex x being set st the carrier of G = {x} )
proofend;
end;

:: deftheorem Def2 defines trivial GROUP_6:def_2_:_
 for G being non empty 1-sorted holds
( G is trivial iff ex x being set st the carrier of G = {x} );

theorem Th10: :: GROUP_6:10
for G being Group holds (1). G is trivial
proofend;

registration
let G be Group;
cluster (1). G ->  trivial ;
coherence
 (1). G is trivial by Th10;
end;

registration
cluster non empty trivial strict unital Group-like associative for multMagma ;
existence
 ex b1 being Group st
( b1 is strict & b1 is trivial )
proofend;
end;

theorem Th11: :: GROUP_6:11
( ( for G being trivial Group holds
( card G = 1 & G is finite ) ) & ( for G being finite Group st card G = 1 holds
G is trivial ) )
proofend;

theorem Th12: :: GROUP_6:12
for G being trivial strict Group holds (1). G = G
proofend;

notation
let G be Group;
let N be normal Subgroup of G;
synonym  Cosets N for  Left_Cosets N;
end;

registration
let G be Group;
let N be normal Subgroup of G;
cluster Cosets N ->  non empty ;
coherence
 not Cosets N is empty by GROUP_2:135;
end;

theorem Th13: :: GROUP_6:13
for G being Group
for x being set
for N being normal Subgroup of G st x in Cosets N holds
ex a being Element of G st
( x = a * N & x = N * a )
proofend;

theorem Th14: :: GROUP_6:14
for G being Group
for a being Element of G
for N being normal Subgroup of G holds
( a * N in Cosets N & N * a in Cosets N )
proofend;

theorem Th15: :: GROUP_6:15
for G being Group
for x being set
for N being normal Subgroup of G st x in Cosets N holds
x is Subset of G ;

theorem Th16: :: GROUP_6:16
for G being Group
for A1, A2 being Subset of G
for N being normal Subgroup of G st A1 in Cosets N & A2 in Cosets N holds
A1 * A2 in Cosets N
proofend;

definition
let G be Group;
let N be normal Subgroup of G;
func CosOp N ->  BinOp of (Cosets N) means :Def3: :: GROUP_6:def 3
 for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
it . (W1,W2) = A1 * A2;
existence
 ex b1 being BinOp of (Cosets N) st
for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b1 . (W1,W2) = A1 * A2
proofend;
uniqueness
 for b1, b2 being BinOp of (Cosets N) st ( for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b1 . (W1,W2) = A1 * A2 ) & ( for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b2 . (W1,W2) = A1 * A2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines CosOp GROUP_6:def_3_:_
 for G being Group
for N being normal Subgroup of G
for b3 being BinOp of (Cosets N) holds
( b3 = CosOp N iff for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b3 . (W1,W2) = A1 * A2 );

definition
let G be Group;
let N be normal Subgroup of G;
funcG ./. N ->  multMagma  equals :: GROUP_6:def 4
 multMagma(# (Cosets N),(CosOp N) #);
correctness
coherence
multMagma(# (Cosets N),(CosOp N) #) is multMagma ;
;
end;

:: deftheorem  defines ./. GROUP_6:def_4_:_
 for G being Group
for N being normal Subgroup of G holds G ./. N = multMagma(# (Cosets N),(CosOp N) #);

registration
let G be Group;
let N be normal Subgroup of G;
clusterG ./. N ->  non empty strict ;
coherence
 ( G ./. N is strict & not G ./. N is empty ) ;
end;

theorem :: GROUP_6:17
for G being Group
for N being normal Subgroup of G holds the carrier of (G ./. N) = Cosets N ;

theorem :: GROUP_6:18
for G being Group
for N being normal Subgroup of G holds the multF of (G ./. N) = CosOp N ;

definition
let G be Group;
let N be normal Subgroup of G;
let S be Element of (G ./. N);
func @ S ->  Subset of G equals :: GROUP_6:def 5
S;
coherence
 S is Subset of G by Th15;
end;

:: deftheorem  defines @ GROUP_6:def_5_:_
 for G being Group
for N being normal Subgroup of G
for S being Element of (G ./. N) holds @ S = S;

theorem :: GROUP_6:19
for G being Group
for N being normal Subgroup of G
for T1, T2 being Element of (G ./. N) holds (@ T1) * (@ T2) = T1 * T2 by Def3;

theorem :: GROUP_6:20
for G being Group
for N being normal Subgroup of G
for T1, T2 being Element of (G ./. N) holds @ (T1 * T2) = (@ T1) * (@ T2) by Def3;

registration
let G be Group;
let N be normal Subgroup of G;
clusterG ./. N ->  Group-like associative ;
coherence
 ( G ./. N is associative & G ./. N is Group-like )
proofend;
end;

theorem :: GROUP_6:21
for G being Group
for N being normal Subgroup of G
for S being Element of (G ./. N) ex a being Element of G st
( S = a * N & S = N * a ) by Th13;

theorem :: GROUP_6:22
for G being Group
for a being Element of G
for N being normal Subgroup of G holds
( N * a is Element of (G ./. N) & a * N is Element of (G ./. N) & carr N is Element of (G ./. N) ) by Th14, GROUP_2:135;

theorem Th23: :: GROUP_6:23
for G being Group
for x being set
for N being normal Subgroup of G holds
( x in G ./. N iff ex a being Element of G st
( x = a * N & x = N * a ) )
proofend;

theorem Th24: :: GROUP_6:24
for G being Group
for N being normal Subgroup of G holds 1_ (G ./. N) = carr N
proofend;

theorem Th25: :: GROUP_6:25
for G being Group
for a being Element of G
for N being normal Subgroup of G
for S being Element of (G ./. N) st S = a * N holds
S " = (a ") * N
proofend;

theorem :: GROUP_6:26
for G being Group
for N being normal Subgroup of G holds card (G ./. N) = Index N ;

theorem :: GROUP_6:27
for G being Group
for N being normal Subgroup of G st Left_Cosets N is finite holds
card (G ./. N) = index N
proofend;

theorem Th28: :: GROUP_6:28
for G being Group
for B being Subgroup of G
for M being strict normal Subgroup of G st M is Subgroup of B holds
B ./. ((B,M) `*`) is Subgroup of G ./. M
proofend;

theorem :: GROUP_6:29
for G being Group
for N, M being strict normal Subgroup of G st M is Subgroup of N holds
N ./. ((N,M) `*`) is normal Subgroup of G ./. M
proofend;

theorem :: GROUP_6:30
for G being strict Group
for N being strict normal Subgroup of G holds
( G ./. N is commutative Group iff G ` is Subgroup of N )
proofend;

Lm1:  for G, H being Group
for a, b being Element of G
for f being Function of the carrier of G, the carrier of H st ( for a being Element of G holds f . a = 1_ H ) holds
f . (a * b) = (f . a) * (f . b)
proofend;

definition
let G, H be non empty multMagma ;
let f be Function of G,H;
attrf is multiplicative  means :Def6: :: GROUP_6:def 6
 for a, b being Element of G holds f . (a * b) = (f . a) * (f . b);
end;

:: deftheorem Def6 defines multiplicative GROUP_6:def_6_:_
 for G, H being non empty multMagma
for f being Function of G,H holds
( f is multiplicative iff for a, b being Element of G holds f . (a * b) = (f . a) * (f . b) );

registration
let G, H be Group;
cluster Relation-like the carrier of G -defined the carrier of H -valued Function-like non empty V22( the carrier of G) quasi_total multiplicative for Element of bool [: the carrier of G, the carrier of H:];
existence
 ex b1 being Function of G,H st b1 is multiplicative
proofend;
end;

definition
let G, H be Group;
mode Homomorphism of G,H is multiplicative Function of G,H;
end;

theorem Th31: :: GROUP_6:31
for G, H being Group
for g being Homomorphism of G,H holds g . (1_ G) = 1_ H
proofend;

registration
let G, H be Group;
cluster Function-like quasi_total multiplicative  ->  unity-preserving for Element of bool [: the carrier of G, the carrier of H:];
coherence
 for b1 being Homomorphism of G,H holds b1 is unity-preserving
proofend;
end;

theorem Th32: :: GROUP_6:32
for G, H being Group
for a being Element of G
for g being Homomorphism of G,H holds g . (a ") = (g . a) "
proofend;

theorem Th33: :: GROUP_6:33
for G, H being Group
for a, b being Element of G
for g being Homomorphism of G,H holds g . (a |^ b) = (g . a) |^ (g . b)
proofend;

theorem Th34: :: GROUP_6:34
for G, H being Group
for a, b being Element of G
for g being Homomorphism of G,H holds g . [.a,b.] = [.(g . a),(g . b).]
proofend;

theorem :: GROUP_6:35
for G, H being Group
for a1, a2, a3 being Element of G
for g being Homomorphism of G,H holds g . [.a1,a2,a3.] = [.(g . a1),(g . a2),(g . a3).]
proofend;

theorem Th36: :: GROUP_6:36
for n being Element of NAT
for G, H being Group
for a being Element of G
for g being Homomorphism of G,H holds g . (a |^ n) = (g . a) |^ n
proofend;

theorem :: GROUP_6:37
for i being Integer
for G, H being Group
for a being Element of G
for g being Homomorphism of G,H holds g . (a |^ i) = (g . a) |^ i
proofend;

theorem Th38: :: GROUP_6:38
for G being Group holds id the carrier of G is multiplicative
proofend;

theorem Th39: :: GROUP_6:39
for G, H, I being Group
for h being Homomorphism of G,H
for h1 being Homomorphism of H,I holds h1 * h is multiplicative
proofend;

registration
let G, H, I be Group;
let h be Homomorphism of G,H;
let h1 be Homomorphism of H,I;
clusterh * h1 ->  multiplicative for Function of G,I;
coherence
 for b1 being Function of G,I st b1 = h1 * h holds
b1 is multiplicative by Th39;
end;

definition
let G, H be Group;
func 1: (G,H) ->  Function of G,H means :Def7: :: GROUP_6:def 7
 for a being Element of G holds it . a = 1_ H;
existence
 ex b1 being Function of G,H st
for a being Element of G holds b1 . a = 1_ H
proofend;
uniqueness
 for b1, b2 being Function of G,H st ( for a being Element of G holds b1 . a = 1_ H ) & ( for a being Element of G holds b2 . a = 1_ H ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines 1: GROUP_6:def_7_:_
 for G, H being Group
for b3 being Function of G,H holds
( b3 = 1: (G,H) iff for a being Element of G holds b3 . a = 1_ H );

registration
let G, H be Group;
cluster 1: (G,H) ->  multiplicative ;
coherence
 1: (G,H) is multiplicative
proofend;
end;

theorem :: GROUP_6:40
for G, H, I being Group
for h being Homomorphism of G,H
for h1 being Homomorphism of H,I holds
( h1 * (1: (G,H)) = 1: (G,I) & (1: (H,I)) * h = 1: (G,I) )
proofend;

definition
let G be Group;
let N be normal Subgroup of G;
func nat_hom N ->  Function of G,(G ./. N) means :Def8: :: GROUP_6:def 8
 for a being Element of G holds it . a = a * N;
existence
 ex b1 being Function of G,(G ./. N) st
for a being Element of G holds b1 . a = a * N
proofend;
uniqueness
 for b1, b2 being Function of G,(G ./. N) st ( for a being Element of G holds b1 . a = a * N ) & ( for a being Element of G holds b2 . a = a * N ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines nat_hom GROUP_6:def_8_:_
 for G being Group
for N being normal Subgroup of G
for b3 being Function of G,(G ./. N) holds
( b3 = nat_hom N iff for a being Element of G holds b3 . a = a * N );

registration
let G be Group;
let N be normal Subgroup of G;
cluster nat_hom N ->  multiplicative ;
coherence
 nat_hom N is multiplicative
proofend;
end;

definition
let G, H be Group;
let g be Homomorphism of G,H;
func Ker g ->  strict Subgroup of G means :Def9: :: GROUP_6:def 9
 the carrier of it =  {  a where a is Element of G : g . a = 1_ H  }  ;
existence
 ex b1 being strict Subgroup of G st the carrier of b1 =  {  a where a is Element of G : g . a = 1_ H  }
proofend;
uniqueness
 for b1, b2 being strict Subgroup of G st the carrier of b1 =  {  a where a is Element of G : g . a = 1_ H  }  & the carrier of b2 =  {  a where a is Element of G : g . a = 1_ H  }  holds
b1 = b2 by GROUP_2:59;
end;

:: deftheorem Def9 defines Ker GROUP_6:def_9_:_
 for G, H being Group
for g being Homomorphism of G,H
for b4 being strict Subgroup of G holds
( b4 = Ker g iff the carrier of b4 =  {  a where a is Element of G : g . a = 1_ H  }  );

registration
let G, H be Group;
let g be Homomorphism of G,H;
cluster Ker g ->  strict normal ;
coherence
 Ker g is normal
proofend;
end;

theorem Th41: :: GROUP_6:41
for G, H being Group
for a being Element of G
for h being Homomorphism of G,H holds
( a in Ker h iff h . a = 1_ H )
proofend;

theorem :: GROUP_6:42
for G, H being strict Group holds Ker (1: (G,H)) = G
proofend;

theorem Th43: :: GROUP_6:43
for G being Group
for N being strict normal Subgroup of G holds Ker (nat_hom N) = N
proofend;

definition
let G, H be Group;
let g be Homomorphism of G,H;
func Image g ->  strict Subgroup of H means :Def10: :: GROUP_6:def 10
 the carrier of it = g .: the carrier of G;
existence
 ex b1 being strict Subgroup of H st the carrier of b1 = g .: the carrier of G
proofend;
uniqueness
 for b1, b2 being strict Subgroup of H st the carrier of b1 = g .: the carrier of G & the carrier of b2 = g .: the carrier of G holds
b1 = b2 by GROUP_2:59;
end;

:: deftheorem Def10 defines Image GROUP_6:def_10_:_
 for G, H being Group
for g being Homomorphism of G,H
for b4 being strict Subgroup of H holds
( b4 = Image g iff the carrier of b4 = g .: the carrier of G );

theorem Th44: :: GROUP_6:44
for G, H being Group
for g being Homomorphism of G,H holds rng g = the carrier of (Image g)
proofend;

theorem Th45: :: GROUP_6:45
for H, G being Group
for x being set
for g being Homomorphism of G,H holds
( x in Image g iff ex a being Element of G st x = g . a )
proofend;

theorem :: GROUP_6:46
for G, H being Group
for g being Homomorphism of G,H holds Image g = gr (rng g)
proofend;

theorem :: GROUP_6:47
for G, H being Group holds Image (1: (G,H)) = (1). H
proofend;

theorem Th48: :: GROUP_6:48
for G being Group
for N being normal Subgroup of G holds Image (nat_hom N) = G ./. N
proofend;

theorem Th49: :: GROUP_6:49
for H, G being Group
for h being Homomorphism of G,H holds h is Homomorphism of G,(Image h)
proofend;

theorem Th50: :: GROUP_6:50
for H, G being Group
for g being Homomorphism of G,H st G is finite holds
Image g is finite
proofend;

registration
let G be finite Group;
let H be Group;
let g be Homomorphism of G,H;
cluster Image g ->  finite strict ;
coherence
 Image g is finite by Th50;
end;

Lm2:  for A being commutative Group
for a, b being Element of A holds a * b = b * a
;

theorem :: GROUP_6:51
for H, G being Group
for g being Homomorphism of G,H st G is commutative Group holds
Image g is commutative
proofend;

theorem Th52: :: GROUP_6:52
for H, G being Group
for g being Homomorphism of G,H holds card (Image g) c= card G
proofend;

theorem :: GROUP_6:53
for G being finite Group
for H being Group
for g being Homomorphism of G,H holds card (Image g) <= card G
proofend;

theorem :: GROUP_6:54
for G, H being Group
for c being Element of H
for h being Homomorphism of G,H st h is one-to-one &amp; c in Image h holds
h . ((h ") . c) = c
proofend;

theorem Th55: :: GROUP_6:55
for H, G being Group
for h being Homomorphism of G,H st h is one-to-one holds
h " is Homomorphism of (Image h),G
proofend;

theorem Th56: :: GROUP_6:56
for H, G being Group
for h being Homomorphism of G,H holds
( h is one-to-one iff Ker h = (1). G )
proofend;

theorem Th57: :: GROUP_6:57
for G being Group
for H being strict Group
for h being Homomorphism of G,H holds
( h is onto iff Image h = H )
proofend;

theorem Th58: :: GROUP_6:58
for G, H being non empty set
for h being Function of G,H st h is onto holds
for c being Element of H ex a being Element of G st h . a = c
proofend;

theorem Th59: :: GROUP_6:59
for G being Group
for N being normal Subgroup of G holds nat_hom N is onto
proofend;

theorem Th60: :: GROUP_6:60
for G, H being set
for h being Function of G,H holds
( h is bijective iff ( rng h = H &amp; h is one-to-one ) )
proofend;

theorem :: GROUP_6:61
for G being set
for H being non empty set
for h being Function of G,H st h is bijective holds
( dom h = G &amp; rng h = H ) by FUNCT_2:def_1, FUNCT_2:def_3;

theorem Th62: :: GROUP_6:62
for G being Group
for H being strict Group
for h being Homomorphism of G,H st h is bijective holds
h " is Homomorphism of H,G
proofend;

theorem Th63: :: GROUP_6:63
for G being set
for H being non empty set
for h being Function of G,H
for g1 being Function of H,G st h is bijective &amp; g1 = h " holds
g1 is bijective
proofend;

theorem Th64: :: GROUP_6:64
for G being set
for H, I being non empty set
for h being Function of G,H
for h1 being Function of H,I st h is bijective &amp; h1 is bijective holds
h1 * h is bijective
proofend;

theorem Th65: :: GROUP_6:65
for G being Group holds nat_hom ((1). G) is bijective
proofend;

definition
let G, H be Group;
predG,H are_isomorphic  means :Def11: :: GROUP_6:def 11
 ex h being Homomorphism of G,H st h is bijective ;
reflexivity
 for G being Group ex h being Homomorphism of G,G st h is bijective
proofend;
end;

:: deftheorem Def11 defines are_isomorphic GROUP_6:def_11_:_
 for G, H being Group holds
( G,H are_isomorphic iff ex h being Homomorphism of G,H st h is bijective );

theorem Th66: :: GROUP_6:66
for G, H being strict Group st G,H are_isomorphic holds
H,G are_isomorphic
proofend;

definition
let G, H be strict Group;
:: original:are_isomorphic
redefine predG,H are_isomorphic ;
symmetry
 for G, H being strict Group st (b1,b2) holds
(b2,b1) by Th66;
end;

theorem :: GROUP_6:67
for G, H, I being Group st G,H are_isomorphic &amp; H,I are_isomorphic holds
G,I are_isomorphic
proofend;

theorem :: GROUP_6:68
for H, G being Group
for h being Homomorphism of G,H st h is one-to-one holds
G, Image h are_isomorphic
proofend;

theorem Th69: :: GROUP_6:69
for G, H being strict Group st G is trivial &amp; H is trivial holds
G,H are_isomorphic
proofend;

theorem :: GROUP_6:70
for G, H being Group holds (1). G, (1). H are_isomorphic by Th69;

theorem :: GROUP_6:71
for G being strict Group holds G,G ./. ((1). G) are_isomorphic
proofend;

theorem :: GROUP_6:72
for G being Group holds G ./. ((Omega). G) is trivial
proofend;

theorem Th73: :: GROUP_6:73
for G, H being strict Group st G,H are_isomorphic holds
card G = card H
proofend;

theorem Th74: :: GROUP_6:74
for G, H being Group st G,H are_isomorphic &amp; G is finite holds
H is finite
proofend;

theorem :: GROUP_6:75
for G, H being strict Group st G,H are_isomorphic &amp; G is finite holds
card G = card H by Th73;

theorem :: GROUP_6:76
for G being trivial strict Group
for H being strict Group st G,H are_isomorphic holds
H is trivial
proofend;

theorem :: GROUP_6:77
for G being Group
for H being strict Group st G,H are_isomorphic &amp; G is commutative holds
H is commutative
proofend;

Lm3:  for H, G being Group
for g being Homomorphism of G,H holds
( G ./. (Ker g), Image g are_isomorphic &amp; ex h being Homomorphism of (G ./. (Ker g)),(Image g) st
( h is bijective &amp; g = h * (nat_hom (Ker g)) ) )
proofend;

theorem :: GROUP_6:78
for H, G being Group
for g being Homomorphism of G,H holds G ./. (Ker g), Image g are_isomorphic by Lm3;

:: [WP: ] First_isomorphism_theorem_for_groups
theorem :: GROUP_6:79
for H, G being Group
for g being Homomorphism of G,H ex h being Homomorphism of (G ./. (Ker g)),(Image g) st
( h is bijective &amp; g = h * (nat_hom (Ker g)) ) by Lm3;

:: [WP: ] Third_isomorphism_theorem_for_groups
theorem :: GROUP_6:80
for G being Group
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) `*`) &amp; M is Subgroup of N holds
(G ./. M) ./. J,G ./. N are_isomorphic
proofend;

:: [WP: ] Second_isomorphism_theorem_for_groups
theorem :: GROUP_6:81
for G being Group
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
proofend;