let R, S, T be Ring; :: thesis: for f being Function of R,S st f is RingHomomorphism holds
for g being Function of S,T st g is RingHomomorphism holds
g * f is RingHomomorphism
let f be Function of R,S; :: thesis: ( f is RingHomomorphism implies for g being Function of S,T st g is RingHomomorphism holds
g * f is RingHomomorphism )
assume A1: f is RingHomomorphism ; :: thesis: for g being Function of S,T st g is RingHomomorphism holds
g * f is RingHomomorphism
let g be Function of S,T; :: thesis: ( g is RingHomomorphism implies g * f is RingHomomorphism )
assume A2: g is RingHomomorphism ; :: thesis: g * f is RingHomomorphism
then A3: for x, y being Element of S holds
( g . (x + y) = (g . x) + (g . y) & g . (x * y) = (g . x) * (g . y) & g . (1_ S) = 1_ T ) by GROUP_1:def 13, GROUP_6:def 6, VECTSP_1:def 20;
A4: for x, y being Element of R holds (g * f) . (x * y) = ((g * f) . x) * ((g * f) . y)

proof

let x, y be Element of R; :: thesis: (g * f) . (x * y) = ((g * f) . x) * ((g * f) . y)
thus (g * f) . (x * y) = g . (f . (x * y)) by FUNCT_2:15
.= g . ((f . x) * (f . y)) by A1, GROUP_6:def 6
.= (g . (f . x)) * (g . (f . y)) by A2, GROUP_6:def 6
.= ((g * f) . x) * (g . (f . y)) by FUNCT_2:15
.= ((g * f) . x) * ((g * f) . y) by FUNCT_2:15 ; :: thesis: verum

end;

A5: for x, y being Element of R holds (g * f) . (x + y) = ((g * f) . x) + ((g * f) . y)

proof

let x, y be Element of R; :: thesis: (g * f) . (x + y) = ((g * f) . x) + ((g * f) . y)
thus (g * f) . (x + y) = g . (f . (x + y)) by FUNCT_2:15
.= g . ((f . x) + (f . y)) by A1, VECTSP_1:def 20
.= (g . (f . x)) + (g . (f . y)) by A2, VECTSP_1:def 20
.= ((g * f) . x) + (g . (f . y)) by FUNCT_2:15
.= ((g * f) . x) + ((g * f) . y) by FUNCT_2:15 ; :: thesis: verum

end;

for x, y being Element of R holds
( f . (x + y) = (f . x) + (f . y) & f . (x * y) = (f . x) * (f . y) & f . (1_ R) = 1_ S ) by A1, GROUP_1:def 13, GROUP_6:def 6, VECTSP_1:def 20;
then A6: (g * f) . (1. R) = 1. T by A3, FUNCT_2:15;
( 1_ R = 1. R & 1_ T = 1. T ) ;
then ( g * f is additive & g * f is multiplicative & g * f is unity-preserving ) by A6, A5, A4, GROUP_1:def 13, GROUP_6:def 6;
hence g * f is RingHomomorphism ; :: thesis: verum