theorem Th6: :: LOPBAN14:5

for X, Y being RealLinearSpace
for f being Function of X,Y holds
( f is LinearOperator of X,Y iff f * ((IsoCPRLSP X) ") is LinearOperator of (product <*X*>),Y )