theorem Th9: :: LOPBAN_1:9

for X being non empty set
for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y)
for a, b being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]