let R be Ring; :: thesis: for G, H being non empty VectSpStr of R
for f being Function of G,H st f is linear holds
f is additive
let G, H be non empty VectSpStr of R; :: thesis: for f being Function of G,H st f is linear holds
f is additive
let f be Function of G,H; :: thesis: ( f is linear implies f is additive )
assume f is linear ; :: thesis: f is additive
then for x, y being Element of G holds f . (x + y) = (f . x) + (f . y) by Def5;
hence f is additive by GRCAT_1:def 13; :: thesis: verum