let K be Field; :: thesis: for V1 being VectSp of K
for f1, f2, f3 being Function of V1,V1 holds (f1 + f2) + f3 = f1 + (f2 + f3)
let V1 be VectSp of K; :: thesis: for f1, f2, f3 being Function of V1,V1 holds (f1 + f2) + f3 = f1 + (f2 + f3)
let f1, f2, f3 be Function of V1,V1; :: thesis: (f1 + f2) + f3 = f1 + (f2 + f3)

A1: now :: thesis: for x being set st x in dom ((f1 + f2) + f3) holds
((f1 + f2) + f3) . x = (f1 + (f2 + f3)) . x

let x be set ; :: thesis: ( x in dom ((f1 + f2) + f3) implies ((f1 + f2) + f3) . x = (f1 + (f2 + f3)) . x )
assume x in dom ((f1 + f2) + f3) ; :: thesis: ((f1 + f2) + f3) . x = (f1 + (f2 + f3)) . x
then reconsider v = x as Element of V1 by FUNCT_2:def 1;
thus ((f1 + f2) + f3) . x = ((f1 + f2) . v) + (f3 . v) by MATRLIN:def 3
.= ((f1 . v) + (f2 . v)) + (f3 . v) by MATRLIN:def 3
.= (f1 . v) + ((f2 . v) + (f3 . v)) by RLVECT_1:def 3
.= (f1 . v) + ((f2 + f3) . v) by MATRLIN:def 3
.= (f1 + (f2 + f3)) . x by MATRLIN:def 3 ; :: thesis: verum

end;

( dom ((f1 + f2) + f3) = [#] V1 & dom (f1 + (f2 + f3)) = [#] V1 ) by FUNCT_2:def 1;
hence (f1 + f2) + f3 = f1 + (f2 + f3) by A1, FUNCT_1:2; :: thesis: verum