let G, H be strict Group; :: thesis: for h being Homomorphism of G,H
for A being strict Subgroup of G
for a, b being Element of G
for H1 being Subgroup of Image h
for a1, b1 being Element of (Image h) st a1 = h . a & b1 = h . b & H1 = h .: A holds
(a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A)
let h be Homomorphism of G,H; :: thesis: for A being strict Subgroup of G
for a, b being Element of G
for H1 being Subgroup of Image h
for a1, b1 being Element of (Image h) st a1 = h . a & b1 = h . b & H1 = h .: A holds
(a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A)
let A be strict Subgroup of G; :: thesis: for a, b being Element of G
for H1 being Subgroup of Image h
for a1, b1 being Element of (Image h) st a1 = h . a & b1 = h . b & H1 = h .: A holds
(a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A)
let a, b be Element of G; :: thesis: for H1 being Subgroup of Image h
for a1, b1 being Element of (Image h) st a1 = h . a & b1 = h . b & H1 = h .: A holds
(a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A)
let H1 be Subgroup of Image h; :: thesis: for a1, b1 being Element of (Image h) st a1 = h . a & b1 = h . b & H1 = h .: A holds
(a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A)
let a1, b1 be Element of (Image h); :: thesis: ( a1 = h . a & b1 = h . b & H1 = h .: A implies (a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A) )
assume that
A1: a1 = h . a and
A2: b1 = h . b and
A3: H1 = h .: A ; :: thesis: (a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A)
A4: a1 * b1 = (h . a) * (h . b) by A1, A2, GROUP_2:52;
set c1 = a1 * b1;
set c = a * b;
A5: h . (a * b) = (h . a) * (h . b) by GROUP_6:def 7;
A6: h .: ((a * b) * A) = (h . (a * b)) * (h .: A) by GRSOLV_1:14;
(a1 * b1) * H1 = (h . (a * b)) * (h .: A)

proof

now

let x be set ; :: thesis: ( x in (a1 * b1) * H1 implies x in (h . (a * b)) * (h .: A) )
assume x in (a1 * b1) * H1 ; :: thesis: x in (h . (a * b)) * (h .: A)
then consider Z being Element of (Image h) such that
A7: x = (a1 * b1) * Z and
A8: Z in H1 by GROUP_2:125;
consider Z1 being Element of A such that
A9: Z = (h | A) . Z1 by A3, A8, GROUP_6:54;
A10: Z1 in A by STRUCT_0:def 5;
reconsider Z1 = Z1 as Element of G by GROUP_2:51;
Z = h . Z1 by A9, FUNCT_1:72;
then A11: x = (h . (a * b)) * (h . Z1) by A4, A5, A7, GROUP_2:52
.= h . ((a * b) * Z1) by GROUP_6:def 7 ;
(a * b) * Z1 in (a * b) * A by A10, GROUP_2:125;
hence x in (h . (a * b)) * (h .: A) by A11, FUNCT_2:43, A6; :: thesis: verum

end;

then A12: (a1 * b1) * H1 c= (h . (a * b)) * (h .: A) by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in (h . (a * b)) * (h .: A) implies x in (a1 * b1) * H1 )
assume x in (h . (a * b)) * (h .: A) ; :: thesis: x in (a1 * b1) * H1
then consider y being set such that
A13: y in the carrier of G and
A14: y in (a * b) * A and
A15: x = h . y by A6, FUNCT_2:115;
reconsider y = y as Element of G by A13;
consider Z being Element of G such that
A16: y = (a * b) * Z and
A17: Z in A by A14, GROUP_2:125;
Z in the carrier of A by A17, STRUCT_0:def 5;
then h . Z in h .: the carrier of A by FUNCT_2:43;
then h . Z in the carrier of (h .: A) by GRSOLV_1:9;
then A18: h . Z in H1 by STRUCT_0:def 5, A3;
then h . Z in Image h by GROUP_2:49;
then reconsider Z1 = h . Z as Element of (Image h) by STRUCT_0:def 5;
A19: x = (h . (a * b)) * (h . Z) by A15, A16, GROUP_6:def 7;
x = (a1 * b1) * Z1 by A19, A4, A5, GROUP_2:52;
hence x in (a1 * b1) * H1 by A18, GROUP_2:125; :: thesis: verum

end;

then (h . (a * b)) * (h .: A) c= (a1 * b1) * H1 by TARSKI:def 3;
hence (a1 * b1) * H1 = (h . (a * b)) * (h .: A) by A12, XBOOLE_0:def 10; :: thesis: verum

end;

hence (a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A) by GROUP_6:def 7; :: thesis: verum