let X be RealNormSpace; :: thesis: 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) ) & 0. (product <*X*>) = I . (0. X) & ( for v being Point of X holds ||.(I . v).|| = ||.v.|| ) )
reconsider X0 = X as RealLinearSpace ;
consider I0 being Function of X0,(product <*X0*>) such that
A1: ( I0 is one-to-one & I0 is onto & ( for x being Point of X holds I0 . x = <*x*> ) & ( for v, w being Point of X0 holds I0 . (v + w) = (I0 . v) + (I0 . w) ) & ( for v being Point of X0
for r being Element of REAL holds I0 . (r * v) = r * (I0 . v) ) & 0. (product <*X0*>) = I0 . (0. X0) ) by Th11;
A2: product <*X*> = NORMSTR(# (product (carr <*X*>)),(zeros <*X*>),[:(addop <*X*>):],[:(multop <*X*>):],(productnorm <*X*>) #) by PRVECT_2:6;
then reconsider I = I0 as Function of X,(product <*X*>) ;
take I ; :: thesis: ( 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) ) & 0. (product <*X*>) = I . (0. X) & ( for v being Point of X holds ||.(I . v).|| = ||.v.|| ) )
thus ( I is one-to-one & I is onto & ( for x being Point of X holds I . x = <*x*> ) ) by A1, A2; :: thesis: ( ( 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) ) & 0. (product <*X*>) = I . (0. X) & ( for v being Point of X holds ||.(I . v).|| = ||.v.|| ) )
thus for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) :: thesis: ( ( for v being Point of X
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & 0. (product <*X*>) = I . (0. X) & ( for v being Point of X holds ||.(I . v).|| = ||.v.|| ) )

proof

let v, w be Point of X; :: thesis: I . (v + w) = (I . v) + (I . w)
reconsider v0 = v, w0 = w as Point of X0 ;
thus I . (v + w) = (I0 . v0) + (I0 . w0) by A1
.= (I . v) + (I . w) by A2 ; :: thesis: verum

end;

thus for v being Point of X
for r being Element of REAL holds I . (r * v) = r * (I . v) :: thesis: ( 0. (product <*X*>) = I . (0. X) & ( for v being Point of X holds ||.(I . v).|| = ||.v.|| ) )

proof

let v be Point of X; :: thesis: for r being Element of REAL holds I . (r * v) = r * (I . v)
let r be Element of REAL ; :: thesis: I . (r * v) = r * (I . v)
reconsider v0 = v as Point of X0 ;
thus I . (r * v) = r * (I0 . v0) by A1
.= r * (I . v) by A2 ; :: thesis: verum

end;

thus 0. (product <*X*>) = I . (0. X) by A1, A2; :: thesis: for v being Point of X holds ||.(I . v).|| = ||.v.||
thus for v being Point of X holds ||.(I . v).|| = ||.v.|| :: thesis: verum

proof

let v be Point of X; :: thesis: ||.(I . v).|| = ||.v.||
A3: len <*||.v.||*> = 1 by FINSEQ_1:40;
reconsider vv = ||.v.|| as Element of REAL ;
reconsider v1 = <*vv*> as Element of REAL 1 by FINSEQ_2:92, A3;
reconsider v2 = ||.v.|| ^2 as Real ;
A4: |.v1.| = sqrt (Sum <*v2*>) by RVSUM_1:55
.= sqrt (||.v.|| ^2) by RVSUM_1:73
.= ||.v.|| by NORMSP_1:4, SQUARE_1:22 ;
A5: I . v = <*v*> by A1;
reconsider Iv = I . v as Element of product (carr <*X*>) by A2;
A6: <*v*> . 1 = v by FINSEQ_1:40;
1 in {1} by TARSKI:def 1;
then reconsider j1 = 1 as Element of dom <*X*> by FINSEQ_1:2, FINSEQ_1:def 8;
A7: (normsequence (<*X*>,Iv)) . j1 = the normF of (<*X*> . j1) . (Iv . j1) by PRVECT_2:def 11
.= ||.v.|| by A5, A6, FINSEQ_1:40 ;
len (normsequence (<*X*>,Iv)) = len <*X*> by PRVECT_2:def 11
.= 1 by FINSEQ_1:40 ;
then normsequence (<*X*>,Iv) = v1 by A7, FINSEQ_1:40;
hence ||.(I . v).|| = ||.v.|| by A4, A2, PRVECT_2:def 12; :: thesis: verum

end;