let O be set ; :: thesis: for G, H being GroupWithOperators of O
for G' being StableSubgroup of G
for H' being StableSubgroup of H
for f being Homomorphism of G,H st ( the carrier of H' = f .: the carrier of G' or the carrier of G' = f " the carrier of H' ) holds
f | the carrier of G' is Homomorphism of G',H'
let G, H be GroupWithOperators of O; :: thesis: for G' being StableSubgroup of G
for H' being StableSubgroup of H
for f being Homomorphism of G,H st ( the carrier of H' = f .: the carrier of G' or the carrier of G' = f " the carrier of H' ) holds
f | the carrier of G' is Homomorphism of G',H'
let G' be StableSubgroup of G; :: thesis: for H' being StableSubgroup of H
for f being Homomorphism of G,H st ( the carrier of H' = f .: the carrier of G' or the carrier of G' = f " the carrier of H' ) holds
f | the carrier of G' is Homomorphism of G',H'
let H' be StableSubgroup of H; :: thesis: for f being Homomorphism of G,H st ( the carrier of H' = f .: the carrier of G' or the carrier of G' = f " the carrier of H' ) holds
f | the carrier of G' is Homomorphism of G',H'
let f be Homomorphism of G,H; :: thesis: ( ( the carrier of H' = f .: the carrier of G' or the carrier of G' = f " the carrier of H' ) implies f | the carrier of G' is Homomorphism of G',H' )
set g = f | the carrier of G';
G' is Subgroup of G by Def7;
then A1: the carrier of G' c= the carrier of G by GROUP_2:def 5;
then A2: the carrier of G' c= dom f by FUNCT_2:def 1;
then A3: dom (f | the carrier of G') = the carrier of G' by RELAT_1:91;
assume A4: ( the carrier of H' = f .: the carrier of G' or the carrier of G' = f " the carrier of H' ) ; :: thesis: f | the carrier of G' is Homomorphism of G',H'
A5: for x being set st x in the carrier of G' holds
f . x in the carrier of H'

proof

let x be set ; :: thesis: ( x in the carrier of G' implies f . x in the carrier of H' )
assume A6: x in the carrier of G' ; :: thesis: f . x in the carrier of H'

per cases ( the carrier of H' = f .: the carrier of G' or the carrier of G' = f " the carrier of H' ) by A4;

suppose A7: the carrier of H' = f .: the carrier of G' ; :: thesis: f . x in the carrier of H'

assume not f . x in the carrier of H' ; :: thesis: contradiction
hence contradiction by A2, A6, A7, FUNCT_1:def 12; :: thesis: verum

end;

suppose the carrier of G' = f " the carrier of H' ; :: thesis: f . x in the carrier of H'

hence f . x in the carrier of H' by A6, FUNCT_1:def 13; :: thesis: verum

end;

end;

end;

now

let y be set ; :: thesis: ( y in rng (f | the carrier of G') implies y in the carrier of H' )
assume y in rng (f | the carrier of G') ; :: thesis: y in the carrier of H'
then consider x being set such that
A8: x in dom (f | the carrier of G') and
A9: y = (f | the carrier of G') . x by FUNCT_1:def 5;
A10: x in the carrier of G' by A2, A8, RELAT_1:91;
then y = f . x by A9, FUNCT_1:72;
hence y in the carrier of H' by A5, A10; :: thesis: verum

end;

then rng (f | the carrier of G') c= the carrier of H' by TARSKI:def 3;
then reconsider g = f | the carrier of G' as Function of G',H' by A3, RELSET_1:11;

A11: now

let a', b' be Element of ; :: thesis: g . (a' * b') = (g . a') * (g . b')
reconsider a = a', b = b' as Element of by A1, TARSKI:def 3;
A12: ( f . a = g . a' & f . b = g . b' ) by FUNCT_1:72;
thus g . (a' * b') = f . (a' * b') by FUNCT_1:72
.= f . (a * b) by Th3
.= (f . a) * (f . b) by GROUP_6:def 7
.= (g . a') * (g . b') by A12, Th3 ; :: thesis: verum

end;

now

let o be Element of O; :: thesis: for a' being Element of holds g . ((G' ^ o) . a') = (H' ^ o) . (g . a')
let a' be Element of ; :: thesis: g . ((G' ^ o) . a') = (H' ^ o) . (g . a')
reconsider a = a' as Element of by A1, TARSKI:def 3;
thus g . ((G' ^ o) . a') = f . ((G' ^ o) . a') by FUNCT_1:72
.= f . (((G ^ o) | the carrier of G') . a') by Def7
.= f . ((G ^ o) . a) by FUNCT_1:72
.= (H ^ o) . (f . a) by Def18
.= (H ^ o) . (g . a') by FUNCT_1:72
.= ((H ^ o) | the carrier of H') . (g . a') by FUNCT_1:72
.= (H' ^ o) . (g . a') by Def7 ; :: thesis: verum

end;

hence f | the carrier of G' is Homomorphism of G',H' by A11, Def18, GROUP_6:def 7; :: thesis: verum