let D be non empty set ; :: thesis: for G being non empty multMagma
for f1, f2 being Element of (.: (G,D))
for a being Element of D holds (f1 * f2) . a = (f1 . a) * (f2 . a)
let G be non empty multMagma ; :: thesis: for f1, f2 being Element of (.: (G,D))
for a being Element of D holds (f1 * f2) . a = (f1 . a) * (f2 . a)
let f1, f2 be Element of (.: (G,D)); :: thesis: for a being Element of D holds (f1 * f2) . a = (f1 . a) * (f2 . a)
let a be Element of D; :: thesis: (f1 * f2) . a = (f1 . a) * (f2 . a)
reconsider g1 = f1, g2 = f2 as Element of Funcs (D,H₃(G)) by Th17;
H₁( .: (G,D)) = (H₁(G),H₃(G)) .: D by Th17;
then ( dom (H₁(G) .: (g1,g2)) = D & f1 * f2 = H₁(G) .: (g1,g2) ) by Def2, FUNCT_2:def 1;
hence (f1 * f2) . a = (f1 . a) * (f2 . a) by FUNCOP_1:22; :: thesis: verum