let R be commutative Ring; :: thesis: for U, V being VectSp of R
for f, g being linear-transformation of U,V holds f '+' g is linear-transformation of U,V
let U, V be VectSp of R; :: thesis: for f, g being linear-transformation of U,V holds f '+' g is linear-transformation of U,V
let f, g be linear-transformation of U,V; :: thesis: f '+' g is linear-transformation of U,V

A: now :: thesis: for x, y being Element of U holds (f '+' g) . (x + y) = ((f '+' g) . x) + ((f '+' g) . y)

let x, y be Element of U; :: thesis: (f '+' g) . (x + y) = ((f '+' g) . x) + ((f '+' g) . y)
thus (f '+' g) . (x + y) = (f . (x + y)) + (g . (x + y)) by defp
.= ((f . x) + (f . y)) + (g . (x + y)) by VECTSP_1:def 20
.= ((f . x) + (f . y)) + ((g . x) + (g . y)) by VECTSP_1:def 20
.= (f . x) + ((f . y) + ((g . x) + (g . y))) by RLVECT_1:def 3
.= (f . x) + (((f . y) + (g . y)) + (g . x)) by RLVECT_1:def 3
.= ((f . x) + (g . x)) + ((f . y) + (g . y)) by RLVECT_1:def 3
.= ((f '+' g) . x) + ((f . y) + (g . y)) by defp
.= ((f '+' g) . x) + ((f '+' g) . y) by defp ; :: thesis: verum

end;

now :: thesis: for a being Element of R
for x being Element of U holds (f '+' g) . (a * x) = a * ((f '+' g) . x)

let a be Element of R; :: thesis: for x being Element of U holds (f '+' g) . (a * x) = a * ((f '+' g) . x)
let x be Element of U; :: thesis: (f '+' g) . (a * x) = a * ((f '+' g) . x)
thus (f '+' g) . (a * x) = (f . (a * x)) + (g . (a * x)) by defp
.= (a * (f . x)) + (g . (a * x)) by MOD_2:def 2
.= (a * (f . x)) + (a * (g . x)) by MOD_2:def 2
.= a * ((f . x) + (g . x)) by VECTSP_1:def 14
.= a * ((f '+' g) . x) by defp ; :: thesis: verum

end;

hence f '+' g is linear-transformation of U,V by A, MOD_2:def 2, VECTSP_1:def 20; :: thesis: verum