let G, H be strict Group; :: thesis: for h being Homomorphism of G,H
for A, B being Subset of G holds (h .: A) * (h .: B) = h .: (A * B)
let h be Homomorphism of G,H; :: thesis: for A, B being Subset of G holds (h .: A) * (h .: B) = h .: (A * B)
let A, B be Subset of G; :: thesis: (h .: A) * (h .: B) = h .: (A * B)

now :: thesis: for z being object st z in (h .: A) * (h .: B) holds
z in h .: (A * B)

let z be object ; :: thesis: ( z in (h .: A) * (h .: B) implies z in h .: (A * B) )
assume z in (h .: A) * (h .: B) ; :: thesis: z in h .: (A * B)
then consider z1, z2 being Element of H such that
A1: z = z1 * z2 and
A2: z1 in h .: A and
A3: z2 in h .: B ;
consider z4 being object such that
A4: z4 in the carrier of G and
A5: z4 in B and
A6: z2 = h . z4 by A3, FUNCT_2:64;
reconsider z4 = z4 as Element of G by A4;
consider z3 being object such that
A7: z3 in the carrier of G and
A8: z3 in A and
A9: z1 = h . z3 by A2, FUNCT_2:64;
reconsider z3 = z3 as Element of G by A7;
A10: z3 * z4 in A * B by A8, A5;
z = h . (z3 * z4) by A1, A9, A6, GROUP_6:def 6;
hence z in h .: (A * B) by A10, FUNCT_2:35; :: thesis: verum

end;

then A11: (h .: A) * (h .: B) c= h .: (A * B) ;

now :: thesis: for z being object st z in h .: (A * B) holds
z in (h .: A) * (h .: B)

let z be object ; :: thesis: ( z in h .: (A * B) implies z in (h .: A) * (h .: B) )
assume z in h .: (A * B) ; :: thesis: z in (h .: A) * (h .: B)
then consider x being object such that
A12: x in the carrier of G and
A13: x in A * B and
A14: z = h . x by FUNCT_2:64;
reconsider x = x as Element of G by A12;
consider z1, z2 being Element of G such that
A15: x = z1 * z2 and
A16: ( z1 in A & z2 in B ) by A13;
A17: ( h . z1 in h .: A & h . z2 in h .: B ) by A16, FUNCT_2:35;
z = (h . z1) * (h . z2) by A14, A15, GROUP_6:def 6;
hence z in (h .: A) * (h .: B) by A17; :: thesis: verum

end;

then h .: (A * B) c= (h .: A) * (h .: B) ;
hence (h .: A) * (h .: B) = h .: (A * B) by A11, XBOOLE_0:def 10; :: thesis: verum