let G, H, I be non empty unital multMagma ; :: thesis: for h being multiplicative Function of G,H
for h1 being multiplicative Function of H,I holds h1 * h is multiplicative
let h be multiplicative Function of G,H; :: thesis: for h1 being multiplicative Function of H,I holds h1 * h is multiplicative
let h1 be multiplicative Function of H,I; :: thesis: h1 * h is multiplicative
set f = h1 * h;
let a, b be Element of G; :: according to GROUP_6:def 6 :: thesis: (h1 * h) . (a * b) = ((h1 * h) . a) * ((h1 * h) . b)
thus (h1 * h) . (a * b) = h1 . (h . (a * b)) by FUNCT_2:15
.= h1 . ((h . a) * (h . b)) by Def6
.= (h1 . (h . a)) * (h1 . (h . b)) by Def6
.= ((h1 * h) . a) * (h1 . (h . b)) by FUNCT_2:15
.= ((h1 * h) . a) * ((h1 * h) . b) by FUNCT_2:15 ; :: thesis: verum