let R be Ring; :: thesis: for E being R -homomorphic Ring
for K being Subring of R
for f being Function of R,E
for g being Function of K,E st g = f | the carrier of K & f is additive holds
g is additive
let E be R -homomorphic Ring; :: thesis: for K being Subring of R
for f being Function of R,E
for g being Function of K,E st g = f | the carrier of K & f is additive holds
g is additive
let K be Subring of R; :: thesis: for f being Function of R,E
for g being Function of K,E st g = f | the carrier of K & f is additive holds
g is additive
let f be Function of R,E; :: thesis: for g being Function of K,E st g = f | the carrier of K & f is additive holds
g is additive
let g be Function of K,E; :: thesis: ( g = f | the carrier of K & f is additive implies g is additive )
assume that
A1: g = f | the carrier of K and
A2: f is additive ; :: thesis: g is additive
let x, y be Element of K; :: according to VECTSP_1:def 19 :: thesis: g . (x + y) = (g . x) + (g . y)
the carrier of K c= the carrier of R by C0SP1:def 3;
then reconsider x1 = x, y1 = y as Element of R ;
A3: x + y = ( the addF of R || the carrier of K) . (x,y) by C0SP1:def 3
.= x1 + y1 by Th1 ;
thus g . (x + y) = f . (x + y) by A1, FUNCT_1:49
.= (f . x1) + (f . y1) by A2, A3
.= (g . x) + (f . y1) by A1, FUNCT_1:49
.= (g . x) + (g . y) by A1, FUNCT_1:49 ; :: thesis: verum