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 Th18;
( H₁( .: G,D) = H₁(G),H₃(G) .: D & f1 * f2 = H₁( .: G,D) . f1,f2 ) by Th18;
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:28; :: thesis: verum