let G, H be strict Group; :: thesis: for h being Homomorphism of G,H
for A being strict Subgroup of G
for a being Element of G holds
( (h . a) * (h .: A) = h .: (a * A) & (h .: A) * (h . a) = h .: (A * a) )
let h be Homomorphism of G,H; :: thesis: for A being strict Subgroup of G
for a being Element of G holds
( (h . a) * (h .: A) = h .: (a * A) & (h .: A) * (h . a) = h .: (A * a) )
let A be strict Subgroup of G; :: thesis: for a being Element of G holds
( (h . a) * (h .: A) = h .: (a * A) & (h .: A) * (h . a) = h .: (A * a) )
let a be Element of G; :: thesis: ( (h . a) * (h .: A) = h .: (a * A) & (h .: A) * (h . a) = h .: (A * a) )

now

let x be set ; :: thesis: ( x in (h . a) * (h .: A) implies x in h .: (a * A) )
assume x in (h . a) * (h .: A) ; :: thesis: x in h .: (a * A)
then consider b1 being Element of H such that
A1: ( x = (h . a) * b1 & b1 in h .: A ) by GROUP_2:125;
consider b being Element of A such that
A2: b1 = (h | A) . b by A1, GROUP_6:54;
A3: b in A by STRUCT_0:def 5;
reconsider b = b as Element of G by GROUP_2:51;
b1 = h . b by A2, FUNCT_1:72;
then A4: x = h . (a * b) by A1, GROUP_6:def 7;
a * b in a * A by A3, GROUP_2:125;
hence x in h .: (a * A) by A4, FUNCT_2:43; :: thesis: verum

end;

then A5: (h . a) * (h .: A) c= h .: (a * A) by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in h .: (a * A) implies x in (h . a) * (h .: A) )
assume x in h .: (a * A) ; :: thesis: x in (h . a) * (h .: A)
then consider y being set such that
A6: ( y in the carrier of G & y in a * A & x = h . y ) by FUNCT_2:115;
reconsider y = y as Element of G by A6;
consider b being Element of G such that
A7: ( y = a * b & b in A ) by A6, GROUP_2:125;
A8: b in the carrier of A by A7, STRUCT_0:def 5;
A9: x = (h . a) * (h . b) by A6, A7, GROUP_6:def 7;
h . b in h .: the carrier of A by A8, FUNCT_2:43;
then h . b in the carrier of (h .: A) by Th9;
then h . b in h .: A by STRUCT_0:def 5;
hence x in (h . a) * (h .: A) by A9, GROUP_2:125; :: thesis: verum

end;

then h .: (a * A) c= (h . a) * (h .: A) by TARSKI:def 3;
hence (h . a) * (h .: A) = h .: (a * A) by A5, XBOOLE_0:def 10; :: thesis: (h .: A) * (h . a) = h .: (A * a)

now

let x be set ; :: thesis: ( x in (h .: A) * (h . a) implies x in h .: (A * a) )
assume x in (h .: A) * (h . a) ; :: thesis: x in h .: (A * a)
then consider b1 being Element of H such that
A10: ( x = b1 * (h . a) & b1 in h .: A ) by GROUP_2:126;
consider b being Element of A such that
A11: b1 = (h | A) . b by A10, GROUP_6:54;
A12: b in A by STRUCT_0:def 5;
reconsider b = b as Element of G by GROUP_2:51;
b1 = h . b by A11, FUNCT_1:72;
then A13: x = h . (b * a) by A10, GROUP_6:def 7;
b * a in A * a by A12, GROUP_2:126;
hence x in h .: (A * a) by A13, FUNCT_2:43; :: thesis: verum

end;

then A14: (h .: A) * (h . a) c= h .: (A * a) by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in h .: (A * a) implies x in (h .: A) * (h . a) )
assume x in h .: (A * a) ; :: thesis: x in (h .: A) * (h . a)
then consider y being set such that
A15: ( y in the carrier of G & y in A * a & x = h . y ) by FUNCT_2:115;
reconsider y = y as Element of G by A15;
consider b being Element of G such that
A16: ( y = b * a & b in A ) by A15, GROUP_2:126;
A17: b in the carrier of A by A16, STRUCT_0:def 5;
A18: x = (h . b) * (h . a) by A15, A16, GROUP_6:def 7;
h . b in h .: the carrier of A by A17, FUNCT_2:43;
then h . b in the carrier of (h .: A) by Th9;
then h . b in h .: A by STRUCT_0:def 5;
hence x in (h .: A) * (h . a) by A18, GROUP_2:126; :: thesis: verum

end;

then h .: (A * a) c= (h .: A) * (h . a) by TARSKI:def 3;
hence (h .: A) * (h . a) = h .: (A * a) by A14, XBOOLE_0:def 10; :: thesis: verum