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]

now

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

end;

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