let R, S, T be Ring; 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; ( 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
; for g being Function of S,T st g is RingHomomorphism holds
g * f is RingHomomorphism
let g be Function of S,T; ( g is RingHomomorphism implies g * f is RingHomomorphism )
assume A2:
g is RingHomomorphism
; 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)
A5:
for x, y being Element of R holds (g * f) . (x + y) = ((g * f) . x) + ((g * f) . y)
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
; verum