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_{3}(G)) by Th17;

H_{1}( .: (G,D)) = (H_{1}(G),H_{3}(G)) .: D
by Th17;

then ( dom (H_{1}(G) .: (g1,g2)) = D & f1 * f2 = H_{1}(G) .: (g1,g2) )
by Def2, FUNCT_2:def 1;

hence (f1 * f2) . a = (f1 . a) * (f2 . a) by FUNCOP_1:22; :: thesis: verum

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

H

then ( dom (H

hence (f1 * f2) . a = (f1 . a) * (f2 . a) by FUNCOP_1:22; :: thesis: verum