let R be Ring; :: thesis: for G, H, S being non empty ModuleStr over R
for f being Function of G,H
for g being Function of H,S st f is homogeneous & g is homogeneous holds
g * f is homogeneous
let G, H, S be non empty ModuleStr over R; :: thesis: for f being Function of G,H
for g being Function of H,S st f is homogeneous & g is homogeneous holds
g * f is homogeneous
let f be Function of G,H; :: thesis: for g being Function of H,S st f is homogeneous & g is homogeneous holds
g * f is homogeneous
let g be Function of H,S; :: thesis: ( f is homogeneous & g is homogeneous implies g * f is homogeneous )
assume that
A1: f is homogeneous and
A2: g is homogeneous ; :: thesis: g * f is homogeneous
set h = g * f;
let a be Scalar of R; :: according to MOD_2:def 2 :: thesis: for x being Vector of G holds (g * f) . (a * x) = a * ((g * f) . x)
let x be Vector of G; :: thesis: (g * f) . (a * x) = a * ((g * f) . x)
thus (g * f) . (a * x) = g . (f . (a * x)) by FUNCT_2:15
.= g . (a * (f . x)) by A1
.= a * (g . (f . x)) by A2
.= a * ((g * f) . x) by FUNCT_2:15 ; :: thesis: verum