let G1, G2, G3 be non empty doubleLoopStr ; :: thesis: for f being Function of G1,G2
for g being Function of G2,G3 st f is linear & g is linear holds
g * f is linear
let f be Function of G1,G2; :: thesis: for g being Function of G2,G3 st f is linear & g is linear holds
g * f is linear
let g be Function of G2,G3; :: thesis: ( f is linear & g is linear implies g * f is linear )
assume that
A1: ( f is additive & f is multiplicative & f is unity-preserving ) and
A2: ( g is additive & g is multiplicative & g is unity-preserving ) ; :: according to RINGCAT1:def 1 :: thesis: g * f is linear
set h = g * f;
thus g * f is additive :: according to RINGCAT1:def 1 :: thesis: ( g * f is multiplicative & g * f is unity-preserving )

proof

let x, y be Scalar of G1; :: according to VECTSP_1:def 19 :: thesis: (g * f) . (x + y) = ((g * f) . x) + ((g * f) . y)
A3: ( g . (f . x) = (g * f) . x & g . (f . y) = (g * f) . y ) by FUNCT_2:15;
thus (g * f) . (x + y) = g . (f . (x + y)) by FUNCT_2:15
.= g . ((f . x) + (f . y)) by A1
.= ((g * f) . x) + ((g * f) . y) by A2, A3 ; :: thesis: verum

end;

thus g * f is multiplicative :: thesis: g * f is unity-preserving

proof

let x, y be Scalar of G1; :: according to GROUP_6:def 6 :: thesis: (g * f) . (x * y) = ((g * f) . x) * ((g * f) . y)
A4: ( g . (f . x) = (g * f) . x & g . (f . y) = (g * f) . y ) by FUNCT_2:15;
thus (g * f) . (x * y) = g . (f . (x * y)) by FUNCT_2:15
.= g . ((f . x) * (f . y)) by A1
.= ((g * f) . x) * ((g * f) . y) by A2, A4 ; :: thesis: verum

end;

thus (g * f) . (1_ G1) = g . (f . (1_ G1)) by FUNCT_2:15
.= g . (1_ G2) by A1
.= 1_ G3 by A2 ; :: according to GROUP_1:def 13 :: thesis: verum