let R be Ring; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( (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 ;
:: thesis: (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 ;
:: thesis: verum