theorem Th8: :: CLOPBAN1:8

for X being non empty set
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]