let X be non empty set ; for Y being ComplexLinearSpace
for f, g, h being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h))) = (FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)
let Y be ComplexLinearSpace; for f, g, h being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h))) = (FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)
let f, g, h be Element of Funcs (X, the carrier of Y); (FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h))) = (FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)
now for x being Element of X holds ((FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h)))) . x = ((FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)) . xlet x be
Element of
X;
((FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h)))) . x = ((FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)) . xthus ((FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h)))) . x =
(f . x) + (((FuncAdd (X,Y)) . (g,h)) . x)
by LOPBAN_1:1
.=
(f . x) + ((g . x) + (h . x))
by LOPBAN_1:1
.=
((f . x) + (g . x)) + (h . x)
by RLVECT_1:def 3
.=
(((FuncAdd (X,Y)) . (f,g)) . x) + (h . x)
by LOPBAN_1:1
.=
((FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)) . x
by LOPBAN_1:1
;
verum end;
hence
(FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h))) = (FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)
by FUNCT_2:63; verum