theorem Th7: :: LOPBAN14:6

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