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 holds
( ((h . a) * (h . b)) * (h .: A) = h .: ((a * b) * A) & ((h .: A) * (h . a)) * (h . b) = h .: ((A * a) * b) )
let h be Homomorphism of G,H; :: thesis: for A being strict Subgroup of G
for a, b being Element of G holds
( ((h . a) * (h . b)) * (h .: A) = h .: ((a * b) * A) & ((h .: A) * (h . a)) * (h . b) = h .: ((A * a) * b) )
let A be strict Subgroup of G; :: thesis: for a, b being Element of G holds
( ((h . a) * (h . b)) * (h .: A) = h .: ((a * b) * A) & ((h .: A) * (h . a)) * (h . b) = h .: ((A * a) * b) )
let a, b be Element of G; :: thesis: ( ((h . a) * (h . b)) * (h .: A) = h .: ((a * b) * A) & ((h .: A) * (h . a)) * (h . b) = h .: ((A * a) * b) )
thus ((h . a) * (h . b)) * (h .: A) = (h . (a * b)) * (h .: A) by GROUP_6:def 6
.= h .: ((a * b) * A) by GRSOLV_1:13 ; :: thesis: ((h .: A) * (h . a)) * (h . b) = h .: ((A * a) * b)
thus ((h .: A) * (h . a)) * (h . b) = (h .: A) * ((h . a) * (h . b)) by GROUP_2:107
.= (h .: A) * (h . (a * b)) by GROUP_6:def 6
.= h .: (A * (a * b)) by GRSOLV_1:13
.= h .: ((A * a) * b) by GROUP_2:107 ; :: thesis: verum