let R be Ring; :: thesis: for G, H, S being non empty VectSpStr of R
for f being Function of G,H
for g being Function of H,S st f is linear & g is linear holds
g * f is linear
let G, H, S be non empty VectSpStr of R; :: thesis: for f being Function of G,H
for g being Function of H,S st f is linear & g is linear holds
g * f is linear
let f be Function of G,H; :: thesis: for g being Function of H,S st f is linear & g is linear holds
g * f is linear
let g be Function of H,S; :: thesis: ( f is linear & g is linear implies g * f is linear )
assume that
A1: f is linear and
A2: g is linear ; :: thesis: g * f is linear
set h = g * f;
A3: ( f is additive & g is additive ) by A1, A2, Th4;
A4: for x, y being Vector of G holds (g * f) . (x + y) = ((g * f) . x) + ((g * f) . y)

proof

let x, y be Vector of G; :: thesis: (g * f) . (x + y) = ((g * f) . x) + ((g * f) . y)
g * f is additive by A3, GRCAT_1:14;
hence (g * f) . (x + y) = ((g * f) . x) + ((g * f) . y) by GRCAT_1:def 13; :: thesis: verum

end;

now

let a be Scalar of R; :: 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:21
.= g . (a * (f . x)) by A1, Def5
.= a * (g . (f . x)) by A2, Def5
.= a * ((g * f) . x) by FUNCT_2:21 ; :: thesis: verum

end;

hence g * f is linear by A4, Def5; :: thesis: verum