let G1, G2, G3 be non empty addMagma ; :: thesis: for f being Function of G1,G2
for g being Function of G2,G3 st f is additive & g is additive holds
g * f is additive
let f be Function of G1,G2; :: thesis: for g being Function of G2,G3 st f is additive & g is additive holds
g * f is additive
let g be Function of G2,G3; :: thesis: ( f is additive & g is additive implies g * f is additive )
assume that
A1: f is additive and
A2: g is additive ; :: thesis: g * f is additive
set h = g * f;

now :: thesis: for x, y being Element of G1 holds (g * f) . (x + y) = ((g * f) . x) + ((g * f) . y)

let x, y be Element of G1; :: thesis: (g * f) . (x + y) = ((g * f) . x) + ((g * f) . y)
A3: ( g . (f . x) = (g * f) . x & g . (f . y) = (g * f) . y ) by FUNCT_2:15;
thus (g * f) . (x + y) = g . (f . (x + y)) by FUNCT_2:15
.= g . ((f . x) + (f . y)) by A1
.= ((g * f) . x) + ((g * f) . y) by A2, A3 ; :: thesis: verum

end;

hence g * f is additive ; :: thesis: verum