theorem Th1: :: LOPBAN15:1

for X, Y being RealLinearSpace
for L being LinearOperator of X,Y
for F being FinSequence of X holds L . (Sum F) = Sum (L * F)