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

for G9 being StableSubgroup of G

for H9 being StableSubgroup of H

for f being Homomorphism of G,H st ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) holds

f | the carrier of G9 is Homomorphism of G9,H9

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

for H9 being StableSubgroup of H

for f being Homomorphism of G,H st ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) holds

f | the carrier of G9 is Homomorphism of G9,H9

let G9 be StableSubgroup of G; :: thesis: for H9 being StableSubgroup of H

for f being Homomorphism of G,H st ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) holds

f | the carrier of G9 is Homomorphism of G9,H9

let H9 be StableSubgroup of H; :: thesis: for f being Homomorphism of G,H st ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) holds

f | the carrier of G9 is Homomorphism of G9,H9

let f be Homomorphism of G,H; :: thesis: ( ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) implies f | the carrier of G9 is Homomorphism of G9,H9 )

set g = f | the carrier of G9;

G9 is Subgroup of G by Def7;

then A1: the carrier of G9 c= the carrier of G by GROUP_2:def 5;

then A2: the carrier of G9 c= dom f by FUNCT_2:def 1;

then A3: dom (f | the carrier of G9) = the carrier of G9 by RELAT_1:62;

assume A4: ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) ; :: thesis: f | the carrier of G9 is Homomorphism of G9,H9

A5: for x being set st x in the carrier of G9 holds

f . x in the carrier of H9

then reconsider g = f | the carrier of G9 as Function of G9,H9 by A3, RELSET_1:4;

for G9 being StableSubgroup of G

for H9 being StableSubgroup of H

for f being Homomorphism of G,H st ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) holds

f | the carrier of G9 is Homomorphism of G9,H9

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

for H9 being StableSubgroup of H

for f being Homomorphism of G,H st ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) holds

f | the carrier of G9 is Homomorphism of G9,H9

let G9 be StableSubgroup of G; :: thesis: for H9 being StableSubgroup of H

for f being Homomorphism of G,H st ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) holds

f | the carrier of G9 is Homomorphism of G9,H9

let H9 be StableSubgroup of H; :: thesis: for f being Homomorphism of G,H st ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) holds

f | the carrier of G9 is Homomorphism of G9,H9

let f be Homomorphism of G,H; :: thesis: ( ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) implies f | the carrier of G9 is Homomorphism of G9,H9 )

set g = f | the carrier of G9;

G9 is Subgroup of G by Def7;

then A1: the carrier of G9 c= the carrier of G by GROUP_2:def 5;

then A2: the carrier of G9 c= dom f by FUNCT_2:def 1;

then A3: dom (f | the carrier of G9) = the carrier of G9 by RELAT_1:62;

assume A4: ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) ; :: thesis: f | the carrier of G9 is Homomorphism of G9,H9

A5: for x being set st x in the carrier of G9 holds

f . x in the carrier of H9

proof

let x be set ; :: thesis: ( x in the carrier of G9 implies f . x in the carrier of H9 )

assume A6: x in the carrier of G9 ; :: thesis: f . x in the carrier of H9

end;assume A6: x in the carrier of G9 ; :: thesis: f . x in the carrier of H9

per cases
( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 )
by A4;

end;

suppose A7:
the carrier of H9 = f .: the carrier of G9
; :: thesis: f . x in the carrier of H9

assume
not f . x in the carrier of H9
; :: thesis: contradiction

hence contradiction by A2, A6, A7, FUNCT_1:def 6; :: thesis: verum

end;hence contradiction by A2, A6, A7, FUNCT_1:def 6; :: thesis: verum

now :: thesis: for y being object st y in rng (f | the carrier of G9) holds

y in the carrier of H9

then
rng (f | the carrier of G9) c= the carrier of H9
;y in the carrier of H9

let y be object ; :: thesis: ( y in rng (f | the carrier of G9) implies y in the carrier of H9 )

assume y in rng (f | the carrier of G9) ; :: thesis: y in the carrier of H9

then consider x being object such that

A8: x in dom (f | the carrier of G9) and

A9: y = (f | the carrier of G9) . x by FUNCT_1:def 3;

A10: x in the carrier of G9 by A2, A8, RELAT_1:62;

then y = f . x by A9, FUNCT_1:49;

hence y in the carrier of H9 by A5, A10; :: thesis: verum

end;assume y in rng (f | the carrier of G9) ; :: thesis: y in the carrier of H9

then consider x being object such that

A8: x in dom (f | the carrier of G9) and

A9: y = (f | the carrier of G9) . x by FUNCT_1:def 3;

A10: x in the carrier of G9 by A2, A8, RELAT_1:62;

then y = f . x by A9, FUNCT_1:49;

hence y in the carrier of H9 by A5, A10; :: thesis: verum

then reconsider g = f | the carrier of G9 as Function of G9,H9 by A3, RELSET_1:4;

A11: now :: thesis: for a9, b9 being Element of G9 holds g . (a9 * b9) = (g . a9) * (g . b9)

let a9, b9 be Element of G9; :: thesis: g . (a9 * b9) = (g . a9) * (g . b9)

reconsider a = a9, b = b9 as Element of G by A1;

A12: ( f . a = g . a9 & f . b = g . b9 ) by FUNCT_1:49;

thus g . (a9 * b9) = f . (a9 * b9) by FUNCT_1:49

.= f . (a * b) by Th3

.= (f . a) * (f . b) by GROUP_6:def 6

.= (g . a9) * (g . b9) by A12, Th3 ; :: thesis: verum

end;reconsider a = a9, b = b9 as Element of G by A1;

A12: ( f . a = g . a9 & f . b = g . b9 ) by FUNCT_1:49;

thus g . (a9 * b9) = f . (a9 * b9) by FUNCT_1:49

.= f . (a * b) by Th3

.= (f . a) * (f . b) by GROUP_6:def 6

.= (g . a9) * (g . b9) by A12, Th3 ; :: thesis: verum

now :: thesis: for o being Element of O

for a9 being Element of G9 holds g . ((G9 ^ o) . a9) = (H9 ^ o) . (g . a9)

hence
f | the carrier of G9 is Homomorphism of G9,H9
by A11, Def18, GROUP_6:def 6; :: thesis: verumfor a9 being Element of G9 holds g . ((G9 ^ o) . a9) = (H9 ^ o) . (g . a9)

let o be Element of O; :: thesis: for a9 being Element of G9 holds g . ((G9 ^ o) . a9) = (H9 ^ o) . (g . a9)

let a9 be Element of G9; :: thesis: g . ((G9 ^ o) . a9) = (H9 ^ o) . (g . a9)

reconsider a = a9 as Element of G by A1;

thus g . ((G9 ^ o) . a9) = f . ((G9 ^ o) . a9) by FUNCT_1:49

.= f . (((G ^ o) | the carrier of G9) . a9) by Def7

.= f . ((G ^ o) . a) by FUNCT_1:49

.= (H ^ o) . (f . a) by Def18

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

.= ((H ^ o) | the carrier of H9) . (g . a9) by FUNCT_1:49

.= (H9 ^ o) . (g . a9) by Def7 ; :: thesis: verum

end;let a9 be Element of G9; :: thesis: g . ((G9 ^ o) . a9) = (H9 ^ o) . (g . a9)

reconsider a = a9 as Element of G by A1;

thus g . ((G9 ^ o) . a9) = f . ((G9 ^ o) . a9) by FUNCT_1:49

.= f . (((G ^ o) | the carrier of G9) . a9) by Def7

.= f . ((G ^ o) . a) by FUNCT_1:49

.= (H ^ o) . (f . a) by Def18

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

.= ((H ^ o) | the carrier of H9) . (g . a9) by FUNCT_1:49

.= (H9 ^ o) . (g . a9) by Def7 ; :: thesis: verum