let R be Ring; for S being R -monomorphic Ring
for f being Monomorphism of R,S
for a, b being Element of rng f holds
( (f ") . (a + b) = ((f ") . a) + ((f ") . b) & (f ") . (a * b) = ((f ") . a) * ((f ") . b) )
let S be R -monomorphic Ring; for f being Monomorphism of R,S
for a, b being Element of rng f holds
( (f ") . (a + b) = ((f ") . a) + ((f ") . b) & (f ") . (a * b) = ((f ") . a) * ((f ") . b) )
let f be Monomorphism of R,S; for a, b being Element of rng f holds
( (f ") . (a + b) = ((f ") . a) + ((f ") . b) & (f ") . (a * b) = ((f ") . a) * ((f ") . b) )
let a, b be Element of rng f; ( (f ") . (a + b) = ((f ") . a) + ((f ") . b) & (f ") . (a * b) = ((f ") . a) * ((f ") . b) )
consider x being object such that
A1:
( x in [#] R & f . x = a )
by FUNCT_2:11;
reconsider x = x as Element of R by A1;
consider y being object such that
A2:
( y in [#] R & f . y = b )
by FUNCT_2:11;
reconsider y = y as Element of R by A2;
A3:
[#] R = dom f
by FUNCT_2:def 1;
then A4:
(f ") . b = y
by A2, FUNCT_1:34;
A5:
[#] R = dom f
by FUNCT_2:def 1;
f . (x + y) = a + b
by A1, A2, VECTSP_1:def 20;
hence (f ") . (a + b) =
x + y
by A5, FUNCT_1:34
.=
((f ") . a) + ((f ") . b)
by A1, A3, A4, FUNCT_1:34
;
(f ") . (a * b) = ((f ") . a) * ((f ") . b)
f . (x * y) = a * b
by A1, A2, GROUP_6:def 6;
hence (f ") . (a * b) =
x * y
by A5, FUNCT_1:34
.=
((f ") . a) * ((f ") . b)
by A1, A3, A4, FUNCT_1:34
;
verum