let V, U, W be Z_Module; :: thesis: for f being linear-transformation of V,U
for g being linear-transformation of U,W holds g * f is linear-transformation of V,W
let f be linear-transformation of V,U; :: thesis: for g being linear-transformation of U,W holds g * f is linear-transformation of V,W
let g be linear-transformation of U,W; :: thesis: g * f is linear-transformation of V,W
set gf = g * f;
for x, y being Element of V holds (g * f) . (x + y) = ((g * f) . x) + ((g * f) . y)

proof

let x, y be Element of V; :: thesis: (g * f) . (x + y) = ((g * f) . x) + ((g * f) . y)
P3: f is additive ;
P4: g is additive ;
thus (g * f) . (x + y) = g . (f . (x + y)) by FUNCT_2:15
.= g . ((f . x) + (f . y)) by P3
.= (g . (f . x)) + (g . (f . y)) by P4
.= ((g * f) . x) + (g . (f . y)) by FUNCT_2:15
.= ((g * f) . x) + ((g * f) . y) by FUNCT_2:15 ; :: thesis: verum

end;

then B1: g * f is additive ;
for a being Element of INT.Ring
for x being Element of V holds (g * f) . (a * x) = a * ((g * f) . x)

proof

let a be Element of INT.Ring; :: thesis: for x being Element of V holds (g * f) . (a * x) = a * ((g * f) . x)
let x be Element of V; :: thesis: (g * f) . (a * x) = a * ((g * f) . x)
P3: f is homogeneous ;
P4: g is homogeneous ;
thus (g * f) . (a * x) = g . (f . (a * x)) by FUNCT_2:15
.= g . (a * (f . x)) by P3
.= a * (g . (f . x)) by P4
.= a * ((g * f) . x) by FUNCT_2:15 ; :: thesis: verum

end;

then g * f is homogeneous ;
hence g * f is linear-transformation of V,W by B1; :: thesis: verum