let X be non empty set ; :: thesis: for Y being ComplexLinearSpace
for f being Element of Funcs (X, the carrier of Y)
for a, b being Complex holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]
let Y be ComplexLinearSpace; :: thesis: for f being Element of Funcs (X, the carrier of Y)
for a, b being Complex holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]
let f be Element of Funcs (X, the carrier of Y); :: thesis: for a, b being Complex holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]
let a, b be Complex; :: thesis: (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]
reconsider a1 = a, b1 = b, ab = a + b as Element of COMPLEX by XCMPLX_0:def 2;

now :: thesis: for x being Element of X holds ((FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a1,f]),((FuncExtMult (X,Y)) . [b1,f]))) . x = ((FuncExtMult (X,Y)) . [ab,f]) . x

let x be Element of X; :: thesis: ((FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a1,f]),((FuncExtMult (X,Y)) . [b1,f]))) . x = ((FuncExtMult (X,Y)) . [ab,f]) . x
thus ((FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a1,f]),((FuncExtMult (X,Y)) . [b1,f]))) . x = (((FuncExtMult (X,Y)) . [a1,f]) . x) + (((FuncExtMult (X,Y)) . [b1,f]) . x) by LOPBAN_1:1
.= (a1 * (f . x)) + (((FuncExtMult (X,Y)) . [b1,f]) . x) by Th2
.= (a * (f . x)) + (b * (f . x)) by Th2
.= (a + b) * (f . x) by CLVECT_1:def 3
.= ((FuncExtMult (X,Y)) . [ab,f]) . x by Th2 ; :: thesis: verum

end;

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