now :: thesis: for a, b being Element of R holds (g * f) . (a + b) = ((g * f) . a) + ((g * f) . b)

let a, b be Element of R; :: thesis: (g * f) . (a + b) = ((g * f) . a) + ((g * f) . b)
A: dom f = the carrier of R by FUNCT_2:def 1;
hence (g * f) . (a + b) = g . (f . (a + b)) by FUNCT_1:13
.= g . ((f . a) + (f . b)) by VECTSP_1:def 20
.= (g . (f . a)) + (g . (f . b)) by VECTSP_1:def 20
.= ((g * f) . a) + (g . (f . b)) by A, FUNCT_1:13
.= ((g * f) . a) + ((g * f) . b) by A, FUNCT_1:13 ;
:: thesis: verum

end;

hence for b₁ being Function of R,T st b₁ = g * f holds
b₁ is additive ; :: thesis: verum