theorem Th11: :: PRVECT_3:11

for X being RealLinearSpace ex I being Function of X,(product <*X*>) st
( I is one-to-one & I is onto & ( for x being Point of X holds I . x = <*x*> ) & ( for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of X
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) )