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 (FuncExtMult (X,Y)) . [a,((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 (FuncExtMult (X,Y)) . [a,((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 (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]
let a, b be Complex; :: thesis: (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]

now

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

end;

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