let K be Field; 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; 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; (f1 + f2) + f3 = f1 + (f2 + f3)
( 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; verum