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
P1: ( 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 ThHOM01AA;
XX: 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 P1, XX; :: 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 P1
.= (I . v) + (I . w) by XX ; :: 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 P1
.= r * (I . v) by XX ; :: thesis: verum

end;

thus 0. (product <*X*>) = I . (0. X) by P1, XX; :: 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.||
len <*||.v.||*> = 1 by FINSEQ_1:57;
then reconsider v1 = <*||.v.||*> as Element of REAL 1 by FINSEQ_2:110;
P54: |.v1.| = sqrt (Sum <*(||.v.|| ^2)*>) by RVSUM_1:81
.= sqrt (||.v.|| ^2) by RVSUM_1:103
.= ||.v.|| by SQUARE_1:89, NORMSP_1:8 ;
P55: I . v = <*v*> by P1;
reconsider Iv = I . v as Element of product (carr <*X*>) by XX;
P58: <*v*> . 1 = v by FINSEQ_1:57;
1 in {1} by TARSKI:def 1;
then reconsider j1 = 1 as Element of dom <*X*> by FINSEQ_1:4, FINSEQ_1:def 8;
X2: (normsequence (<*X*>,Iv)) . j1 = the normF of (<*X*> . j1) . (Iv . j1) by PRVECT_2:def 11
.= ||.v.|| by P55, P58, FINSEQ_1:57 ;
len (normsequence (<*X*>,Iv)) = len <*X*> by PRVECT_2:def 11
.= 1 by FINSEQ_1:57 ;
then normsequence (<*X*>,Iv) = v1 by X2, FINSEQ_1:57;
hence ||.(I . v).|| = ||.v.|| by P54, XX, PRVECT_2:def 12; :: thesis: verum

end;