let K be Field; :: thesis: for V1 being VectSp of K
for f1, f2, g being Function of V1,V1 st g is linear holds
g * (f1 + f2) = (g * f1) + (g * f2)
let V1 be VectSp of K; :: thesis: for f1, f2, g being Function of V1,V1 st g is linear holds
g * (f1 + f2) = (g * f1) + (g * f2)
let f1, f2, g be Function of V1,V1; :: thesis: ( g is linear implies g * (f1 + f2) = (g * f1) + (g * f2) )
assume A1: g is linear ; :: thesis: g * (f1 + f2) = (g * f1) + (g * f2)
A2: ( dom (g * (f1 + f2)) = [#] V1 & dom ((g * f1) + (g * f2)) = [#] V1 & dom f1 = [#] V1 & dom f2 = [#] V1 ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in dom (g * (f1 + f2)) implies (g * (f1 + f2)) . x = ((g * f1) + (g * f2)) . x )
assume A3: x in dom (g * (f1 + f2)) ; :: thesis: (g * (f1 + f2)) . x = ((g * f1) + (g * f2)) . x
reconsider v = x as Element of V1 by A3, FUNCT_2:def 1;
thus (g * (f1 + f2)) . x = g . ((f1 + f2) . v) by A2, FUNCT_1:22
.= g . ((f1 . v) + (f2 . v)) by MATRLIN:def 5
.= (g . (f1 . v)) + (g . (f2 . v)) by A1, MOD_2:def 5
.= ((g * f1) . v) + (g . (f2 . v)) by A2, FUNCT_1:23
.= ((g * f1) . v) + ((g * f2) . v) by A2, FUNCT_1:23
.= ((g * f1) + (g * f2)) . x by MATRLIN:def 5 ; :: thesis: verum

end;

hence g * (f1 + f2) = (g * f1) + (g * f2) by A2, FUNCT_1:9; :: thesis: verum