let X be non empty set ; :: thesis: 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; :: thesis: 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); :: thesis: (FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h))) = (FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)

now :: thesis: 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)) . x

let x be Element of X; :: thesis: ((FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h)))) . x = ((FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)) . x
thus ((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 ; :: thesis: 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; :: thesis: verum