let R be Ring; :: thesis: for V, U, W being LeftMod of R
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 V, U, W be LeftMod of R; :: 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 a being Element of R
for x being Element of V holds (g * f) . (a * x) = a * ((g * f) . x)

proof

let a be Element of R; :: 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 ; :: thesis: verum