let X be non empty set ; :: thesis: for Y being ComplexLinearSpace
for f, g being Element of Funcs (X, the carrier of Y)
for a being Complex holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]
let Y be ComplexLinearSpace; :: thesis: for f, g being Element of Funcs (X, the carrier of Y)
for a being Complex holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]
let f, g be Element of Funcs (X, the carrier of Y); :: thesis: for a being Complex holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]
let a be Complex; :: thesis: (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]

now

let x be Element of X; :: thesis: ((FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g]))) . x = ((FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]) . x
thus ((FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g]))) . x = (((FuncExtMult (X,Y)) . [a,f]) . x) + (((FuncExtMult (X,Y)) . [a,g]) . x) by LOPBAN_1:1
.= (a * (f . x)) + (((FuncExtMult (X,Y)) . [a,g]) . x) by Th3
.= (a * (f . x)) + (a * (g . x)) by Th3
.= a * ((f . x) + (g . x)) by CLVECT_1:def 2
.= a * (((FuncAdd (X,Y)) . (f,g)) . x) by LOPBAN_1:1
.= ((FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]) . x by Th3 ; :: thesis: verum

end;

hence (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))] by FUNCT_2:63; :: thesis: verum