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' )
assume A1: ( 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'
G' is Subgroup of G by Def7;
then A2: the carrier of G' c= the carrier of G by GROUP_2:def 5;
then A3: the carrier of G' c= dom f by FUNCT_2:def 1;
A4: 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 A5: 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 A1;

suppose A6: 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 A3, A5, A6, 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 A5, FUNCT_1:def 13; :: thesis: verum

end;

end;

end;

set g = f | the carrier of G';

now

A7: dom (f | the carrier of G') = the carrier of G' by A3, RELAT_1:91;

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') & y = (f | the carrier of G') . x ) by FUNCT_1:def 5;
A9: x in the carrier of G' by A3, A8, RELAT_1:91;
then y = f . x by A8, FUNCT_1:72;
hence y in the carrier of H' by A4, A9; :: thesis: verum

end;

then rng (f | the carrier of G') c= the carrier of H' by TARSKI:def 3;
hence f | the carrier of G' is Function of G',H' by A7, RELSET_1:11; :: thesis: verum

end;

then reconsider g = f | the carrier of G' as Function of G',H' ;

A10: now

let a', b' be Element of G'; :: thesis: g . (a' * b') = (g . a') * (g . b')
reconsider a = a', b = b' as Element of G by A2, TARSKI:def 3;
A11: ( 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 A11, Th3 ; :: thesis: verum

end;

now

let o be Element of O; :: thesis: for a' being Element of G' holds g . ((G' ^ o) . a') = (H' ^ o) . (g . a')
let a' be Element of G'; :: thesis: g . ((G' ^ o) . a') = (H' ^ o) . (g . a')
reconsider a = a' as Element of G by A2, 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 A10, Def18, GROUP_6:def 7; :: thesis: verum