let O be set ; :: thesis: for G, H being GroupWithOperators of O

for h being Homomorphism of G,H holds G ./. (Ker h), Image h are_isomorphic

let G, H be GroupWithOperators of O; :: thesis: for h being Homomorphism of G,H holds G ./. (Ker h), Image h are_isomorphic

let h be Homomorphism of G,H; :: thesis: G ./. (Ker h), Image h are_isomorphic

reconsider G9 = G, H9 = H as Group ;

reconsider h9 = h as Homomorphism of G9,H9 ;

consider g9 being Homomorphism of (G9 ./. (Ker h9)),(Image h9) such that

A1: g9 is bijective and

A2: h9 = g9 * (nat_hom (Ker h9)) by GROUP_6:79;

A3: the carrier of (Image h9) = h9 .: the carrier of G9 by GROUP_6:def 10

.= the carrier of (Image h) by Def22 ;

Ker h is Subgroup of G by Def7;

then A5: multMagma(# the carrier of (Ker h9), the multF of (Ker h9) #) = multMagma(# the carrier of (Ker h), the multF of (Ker h) #) by A4, GROUP_2:59;

then the carrier of (G9 ./. (Ker h9)) = the carrier of (G ./. (Ker h)) by Def14;

then reconsider g = g9 as Function of (G ./. (Ker h)),(Image h) by A3;

Image h is Subgroup of H by Def7;

then A6: multMagma(# the carrier of (Image h9), the multF of (Image h9) #) = multMagma(# the carrier of (Image h), the multF of (Image h) #) by A3, GROUP_2:59;

g is onto by A1, A3;

hence G ./. (Ker h), Image h are_isomorphic by A1; :: thesis: verum

for h being Homomorphism of G,H holds G ./. (Ker h), Image h are_isomorphic

let G, H be GroupWithOperators of O; :: thesis: for h being Homomorphism of G,H holds G ./. (Ker h), Image h are_isomorphic

let h be Homomorphism of G,H; :: thesis: G ./. (Ker h), Image h are_isomorphic

reconsider G9 = G, H9 = H as Group ;

reconsider h9 = h as Homomorphism of G9,H9 ;

consider g9 being Homomorphism of (G9 ./. (Ker h9)),(Image h9) such that

A1: g9 is bijective and

A2: h9 = g9 * (nat_hom (Ker h9)) by GROUP_6:79;

A3: the carrier of (Image h9) = h9 .: the carrier of G9 by GROUP_6:def 10

.= the carrier of (Image h) by Def22 ;

now :: thesis: for x being object holds

( ( x in the carrier of (Ker h) implies x in the carrier of (Ker h9) ) & ( x in the carrier of (Ker h9) implies x in the carrier of (Ker h) ) )

then A4:
the carrier of (Ker h9) = the carrier of (Ker h)
by TARSKI:2;( ( x in the carrier of (Ker h) implies x in the carrier of (Ker h9) ) & ( x in the carrier of (Ker h9) implies x in the carrier of (Ker h) ) )

let x be object ; :: thesis: ( ( x in the carrier of (Ker h) implies x in the carrier of (Ker h9) ) & ( x in the carrier of (Ker h9) implies x in the carrier of (Ker h) ) )

then x in { a9 where a9 is Element of G9 : h9 . a9 = 1_ H9 } by GROUP_6:def 9;

hence x in the carrier of (Ker h) by Def21; :: thesis: verum

end;hereby :: thesis: ( x in the carrier of (Ker h9) implies x in the carrier of (Ker h) )

assume
x in the carrier of (Ker h9)
; :: thesis: x in the carrier of (Ker h)assume
x in the carrier of (Ker h)
; :: thesis: x in the carrier of (Ker h9)

then x in { a where a is Element of G : h . a = 1_ H } by Def21;

hence x in the carrier of (Ker h9) by GROUP_6:def 9; :: thesis: verum

end;then x in { a where a is Element of G : h . a = 1_ H } by Def21;

hence x in the carrier of (Ker h9) by GROUP_6:def 9; :: thesis: verum

then x in { a9 where a9 is Element of G9 : h9 . a9 = 1_ H9 } by GROUP_6:def 9;

hence x in the carrier of (Ker h) by Def21; :: thesis: verum

Ker h is Subgroup of G by Def7;

then A5: multMagma(# the carrier of (Ker h9), the multF of (Ker h9) #) = multMagma(# the carrier of (Ker h), the multF of (Ker h) #) by A4, GROUP_2:59;

then the carrier of (G9 ./. (Ker h9)) = the carrier of (G ./. (Ker h)) by Def14;

then reconsider g = g9 as Function of (G ./. (Ker h)),(Image h) by A3;

Image h is Subgroup of H by Def7;

then A6: multMagma(# the carrier of (Image h9), the multF of (Image h9) #) = multMagma(# the carrier of (Image h), the multF of (Image h) #) by A3, GROUP_2:59;

A7: now :: thesis: for a, b being Element of (G ./. (Ker h)) holds g . (a * b) = (g . a) * (g . b)

let a, b be Element of (G ./. (Ker h)); :: thesis: g . (a * b) = (g . a) * (g . b)

reconsider b9 = b as Element of (G9 ./. (Ker h9)) by A5, Def14;

reconsider a9 = a as Element of (G9 ./. (Ker h9)) by A5, Def14;

thus g . (a * b) = g9 . (a9 * b9) by A5, Def15

.= (g9 . a9) * (g9 . b9) by GROUP_6:def 6

.= (g . a) * (g . b) by A6 ; :: thesis: verum

end;reconsider b9 = b as Element of (G9 ./. (Ker h9)) by A5, Def14;

reconsider a9 = a as Element of (G9 ./. (Ker h9)) by A5, Def14;

thus g . (a * b) = g9 . (a9 * b9) by A5, Def15

.= (g9 . a9) * (g9 . b9) by GROUP_6:def 6

.= (g . a) * (g . b) by A6 ; :: thesis: verum

now :: thesis: for o being Element of O

for a being Element of (G ./. (Ker h)) holds g . (((G ./. (Ker h)) ^ o) . a) = ((Image h) ^ o) . (g . a)

then reconsider g = g as Homomorphism of (G ./. (Ker h)),(Image h) by A7, Def18, GROUP_6:def 6;for a being Element of (G ./. (Ker h)) holds g . (((G ./. (Ker h)) ^ o) . a) = ((Image h) ^ o) . (g . a)

let o be Element of O; :: thesis: for a being Element of (G ./. (Ker h)) holds g . (((G ./. (Ker h)) ^ b_{2}) . b_{3}) = ((Image h) ^ b_{2}) . (g . b_{3})

let a be Element of (G ./. (Ker h)); :: thesis: g . (((G ./. (Ker h)) ^ b_{1}) . b_{2}) = ((Image h) ^ b_{1}) . (g . b_{2})

end;let a be Element of (G ./. (Ker h)); :: thesis: g . (((G ./. (Ker h)) ^ b

per cases
( O is empty or not O is empty )
;

end;

suppose A8:
O is empty
; :: thesis: g . (((G ./. (Ker h)) ^ b_{1}) . b_{2}) = ((Image h) ^ b_{1}) . (g . b_{2})

hence g . (((G ./. (Ker h)) ^ o) . a) =
g . ((id the carrier of (G ./. (Ker h))) . a)
by Def6

.= (id the carrier of (Image h)) . (g . a)

.= ((Image h) ^ o) . (g . a) by A8, Def6 ;

:: thesis: verum

end;.= (id the carrier of (Image h)) . (g . a)

.= ((Image h) ^ o) . (g . a) by A8, Def6 ;

:: thesis: verum

suppose A9:
not O is empty
; :: thesis: g . (((G ./. (Ker h)) ^ b_{1}) . b_{2}) = ((Image h) ^ b_{1}) . (g . b_{2})

reconsider G99 = G ./. (Ker h) as Group ;

set f = the action of (G ./. (Ker h)) . o;

A10: the action of (G ./. (Ker h)) . o = { [A,B] where A, B is Element of Cosets (Ker h) : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } by A9, Def16;

the action of (G ./. (Ker h)) . o = (G ./. (Ker h)) ^ o by A9, Def6;

then reconsider f = the action of (G ./. (Ker h)) . o as Homomorphism of G99,G99 ;

a in the carrier of G99 ;

then a in dom f by FUNCT_2:def 1;

then [a,(f . a)] in f by FUNCT_1:1;

then consider A, B being Element of Cosets (Ker h) such that

A11: [A,B] = [a,(f . a)] and

A12: ex g1, g2 being Element of G st

( g1 in A & g2 in B & g2 = (G ^ o) . g1 ) by A10;

reconsider A = A, B = B as Element of Cosets (Ker h9) by A5, Def14;

consider g1, g2 being Element of G9 such that

A13: g1 in A and

A14: g2 in B and

A15: g2 = (G ^ o) . g1 by A12;

A16: A = g1 * (Ker h9) by A13, Lm8;

g1 in the carrier of G9 ;

then A17: g1 in dom (nat_hom (Ker h9)) by FUNCT_2:def 1;

g2 in the carrier of G9 ;

then A18: g2 in dom (nat_hom (Ker h9)) by FUNCT_2:def 1;

A19: ((Image h) ^ o) . (g . a) = ((H ^ o) | the carrier of (Image h)) . (g . a) by Def7

.= (H ^ o) . (g . a) by FUNCT_1:49

.= (H ^ o) . (g9 . (g1 * (Ker h9))) by A11, A16, XTUPLE_0:1 ;

A20: B = g2 * (Ker h9) by A14, Lm8;

h9 . g2 = (H ^ o) . (h9 . g1) by A15, Def18;

then g9 . ((nat_hom (Ker h9)) . g2) = (H ^ o) . ((g9 * (nat_hom (Ker h9))) . g1) by A2, A18, FUNCT_1:13;

then g9 . ((nat_hom (Ker h9)) . g2) = (H ^ o) . (g9 . ((nat_hom (Ker h9)) . g1)) by A17, FUNCT_1:13;

then A21: g9 . (g2 * (Ker h9)) = (H ^ o) . (g9 . ((nat_hom (Ker h9)) . g1)) by GROUP_6:def 8;

g . (((G ./. (Ker h)) ^ o) . a) = g . (f . a) by A9, Def6

.= g9 . (g2 * (Ker h9)) by A11, A20, XTUPLE_0:1 ;

hence g . (((G ./. (Ker h)) ^ o) . a) = ((Image h) ^ o) . (g . a) by A19, A21, GROUP_6:def 8; :: thesis: verum

end;set f = the action of (G ./. (Ker h)) . o;

A10: the action of (G ./. (Ker h)) . o = { [A,B] where A, B is Element of Cosets (Ker h) : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } by A9, Def16;

the action of (G ./. (Ker h)) . o = (G ./. (Ker h)) ^ o by A9, Def6;

then reconsider f = the action of (G ./. (Ker h)) . o as Homomorphism of G99,G99 ;

a in the carrier of G99 ;

then a in dom f by FUNCT_2:def 1;

then [a,(f . a)] in f by FUNCT_1:1;

then consider A, B being Element of Cosets (Ker h) such that

A11: [A,B] = [a,(f . a)] and

A12: ex g1, g2 being Element of G st

( g1 in A & g2 in B & g2 = (G ^ o) . g1 ) by A10;

reconsider A = A, B = B as Element of Cosets (Ker h9) by A5, Def14;

consider g1, g2 being Element of G9 such that

A13: g1 in A and

A14: g2 in B and

A15: g2 = (G ^ o) . g1 by A12;

A16: A = g1 * (Ker h9) by A13, Lm8;

g1 in the carrier of G9 ;

then A17: g1 in dom (nat_hom (Ker h9)) by FUNCT_2:def 1;

g2 in the carrier of G9 ;

then A18: g2 in dom (nat_hom (Ker h9)) by FUNCT_2:def 1;

A19: ((Image h) ^ o) . (g . a) = ((H ^ o) | the carrier of (Image h)) . (g . a) by Def7

.= (H ^ o) . (g . a) by FUNCT_1:49

.= (H ^ o) . (g9 . (g1 * (Ker h9))) by A11, A16, XTUPLE_0:1 ;

A20: B = g2 * (Ker h9) by A14, Lm8;

h9 . g2 = (H ^ o) . (h9 . g1) by A15, Def18;

then g9 . ((nat_hom (Ker h9)) . g2) = (H ^ o) . ((g9 * (nat_hom (Ker h9))) . g1) by A2, A18, FUNCT_1:13;

then g9 . ((nat_hom (Ker h9)) . g2) = (H ^ o) . (g9 . ((nat_hom (Ker h9)) . g1)) by A17, FUNCT_1:13;

then A21: g9 . (g2 * (Ker h9)) = (H ^ o) . (g9 . ((nat_hom (Ker h9)) . g1)) by GROUP_6:def 8;

g . (((G ./. (Ker h)) ^ o) . a) = g . (f . a) by A9, Def6

.= g9 . (g2 * (Ker h9)) by A11, A20, XTUPLE_0:1 ;

hence g . (((G ./. (Ker h)) ^ o) . a) = ((Image h) ^ o) . (g . a) by A19, A21, GROUP_6:def 8; :: thesis: verum

g is onto by A1, A3;

hence G ./. (Ker h), Image h are_isomorphic by A1; :: thesis: verum