let X be finite-dimensional RealLinearSpace; :: thesis: ( product <*X*> is finite-dimensional & dim (product <*X*>) = dim X )
consider I being Function of X,(product <*X*>) such that
A1: ( I is one-to-one & I is onto ) and
for x being Point of X holds I . x = <*x*> and
A2: for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) and
A3: for v being Point of X
for r being Element of REAL holds I . (r * v) = r * (I . v) and
I . (0. X) = 0. (product <*X*>) by PRVECT_3:11;
A4: I is additive by A2;
for x being VECTOR of X
for r being Real holds I . (r * x) = r * (I . x)

proof

let x be VECTOR of X; :: thesis: for r being Real holds I . (r * x) = r * (I . x)
let r be Real; :: thesis: I . (r * x) = r * (I . x)
reconsider r0 = r as Element of REAL by XREAL_0:def 1;
thus I . (r * x) = r0 * (I . x) by A3
.= r * (I . x) ; :: thesis: verum

end;

then I is LinearOperator of X,(product <*X*>) by A4, LOPBAN_1:def 5;
hence ( product <*X*> is finite-dimensional & dim (product <*X*>) = dim X ) by A1, REAL_NS2:88; :: thesis: verum