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

proof

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

end;

thus for v being Point of [:X,Y:]
for r being Real holds I . (r * v) = r * (I . v) :: thesis: ( 0. (product <*X,Y*>) = I . (0. [:X,Y:]) & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )

proof

let v be Point of [:X,Y:]; :: thesis: for r being Real holds I . (r * v) = r * (I . v)
let r be Real; :: thesis: I . (r * v) = r * (I . v)
reconsider v0 = v as Point of [:X0,Y0:] ;
thus I . (r * v) = I0 . (r * v0)
.= r * (I0 . v0) by A1
.= r * (I . v) by A2 ; :: thesis: verum

end;

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

proof

let v be Point of [:X,Y:]; :: thesis: ||.(I . v).|| = ||.v.||
consider x1 being Point of X, y1 being Point of Y such that
A3: v = [x1,y1] by Lm1;
consider v1 being Element of REAL 2 such that
A4: ( v1 = <*||.x1.||,||.y1.||*> & (prod_NORM (X,Y)) . (x1,y1) = |.v1.| ) by Def6;
A5: I . v = I . (x1,y1) by A3
.= <*x1,y1*> by A1 ;
reconsider Iv = I . v as Element of product (carr <*X,Y*>) by A2;
( 1 in {1,2} & 2 in {1,2} ) by TARSKI:def 2;
then reconsider j1 = 1, j2 = 2 as Element of dom <*X,Y*> by FINSEQ_1:2, FINSEQ_1:89;
A7: (normsequence (<*X,Y*>,Iv)) . j1 = the normF of (<*X,Y*> . j1) . (Iv . j1) by PRVECT_2:def 11
.= ||.x1.|| by A5 ;
A8: (normsequence (<*X,Y*>,Iv)) . j2 = the normF of (<*X,Y*> . j2) . (Iv . j2) by PRVECT_2:def 11
.= ||.y1.|| by A5 ;
len (normsequence (<*X,Y*>,Iv)) = len <*X,Y*> by PRVECT_2:def 11
.= 2 by FINSEQ_1:44 ;
then normsequence (<*X,Y*>,Iv) = v1 by A4, A7, A8, FINSEQ_1:44;
hence ||.(I . v).|| = ||.v.|| by A4, A3, A2, PRVECT_2:def 12; :: thesis: verum

end;

hence for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ; :: thesis: verum