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
A3: ( f is additive & f is multiplicative & f is unity-preserving ) by A1;
then A4: 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 GRCAT_1:def 13, GROUP_1:def 17, GROUP_6:def 7;
A5: ( 1_ R = 1. R & 1_ T = 1. T ) ;
A6: ( g is additive & g is multiplicative & g is unity-preserving ) by A2;
then 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 GRCAT_1:def 13, GROUP_1:def 17, GROUP_6:def 7;
then A7: (g * f) . (1. R) = 1. T by A4, FUNCT_2:21;
A8: 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:21
.= g . ((f . x) + (f . y)) by A3, GRCAT_1:def 13
.= (g . (f . x)) + (g . (f . y)) by A6, GRCAT_1:def 13
.= ((g * f) . x) + (g . (f . y)) by FUNCT_2:21
.= ((g * f) . x) + ((g * f) . y) by FUNCT_2:21 ; :: thesis: verum

end;

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:21
.= g . ((f . x) * (f . y)) by A3, GROUP_6:def 7
.= (g . (f . x)) * (g . (f . y)) by A6, GROUP_6:def 7
.= ((g * f) . x) * (g . (f . y)) by FUNCT_2:21
.= ((g * f) . x) * ((g * f) . y) by FUNCT_2:21 ; :: thesis: verum

end;

then ( g * f is additive & g * f is multiplicative & g * f is unity-preserving ) by A5, A7, A8, GRCAT_1:def 13, GROUP_1:def 17, GROUP_6:def 7;
hence g * f is RingHomomorphism ; :: thesis: verum