consider I being Function of X,(product <*X*>) such that
( I is one-to-one & I is onto ) and
A1: 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
0. (product <*X*>) = I . (0. X) by PRVECT_3:11;

now :: thesis: for v being Point of X
for r being Real holds I . (r * v) = r * (I . v)

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

end;

then reconsider I = I as LinearOperator of X,(product <*X*>) by A2, LOPBAN_1:def 5, VECTSP_1:def 20;
take I ; :: thesis: for x being Point of X holds I . x = <*x*>
thus for x being Point of X holds I . x = <*x*> by A1; :: thesis: verum