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

let z be set ; :: 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 & z1 in h .: A & z2 in h .: B ) ;
consider z3 being set such that
A2: ( z3 in the carrier of G & z3 in A & z1 = h . z3 ) by A1, FUNCT_2:115;
consider z4 being set such that
A3: ( z4 in the carrier of G & z4 in B & z2 = h . z4 ) by A1, FUNCT_2:115;
reconsider z3 = z3 as Element of G by A2;
reconsider z4 = z4 as Element of G by A3;
A4: z = h . (z3 * z4) by A1, A2, A3, GROUP_6:def 7;
z3 * z4 in A * B by A2, A3;
hence z in h .: (A * B) by A4, FUNCT_2:43; :: thesis: verum

end;

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

now

let z be set ; :: 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 set such that
A6: ( x in the carrier of G & x in A * B & z = h . x ) by FUNCT_2:115;
reconsider x = x as Element of G by A6;
consider z1, z2 being Element of G such that
A7: ( x = z1 * z2 & z1 in A & z2 in B ) by A6;
A8: z = (h . z1) * (h . z2) by A6, A7, GROUP_6:def 7;
( h . z1 in h .: A & h . z2 in h .: B ) by A7, FUNCT_2:43;
hence z in (h .: A) * (h .: B) by A8; :: thesis: verum

end;

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