theorem Th86: :: REAL_NS2:86

for X, Y, Z being RealLinearSpace
for L being LinearOperator of X,Y
for K being LinearOperator of Y,Z holds K * L is LinearOperator of X,Z