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

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