theorem Th16: :: PDIFF_6:16

for n, m being Nat
for f being LinearOperator of m,n
for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL n st len xseq = len yseq & ( for i being Nat st i in dom xseq holds
yseq . i = f . (xseq . i) ) holds
Sum yseq = f . (Sum xseq)