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 Element of 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
P1: ( 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 Element of REAL holds I0 . (r * v) = r * (I0 . v) ) & 0. (product <*X0,Y0*>) = I0 . (0. [:X0,Y0:]) ) by ThHOM01;
XX: 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 Element of 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 P1, XX; :: 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 Element of 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 Element of 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 P1
.= (I . v) + (I . w) by XX ; :: thesis: verum

end;

thus for v being Point of [:X,Y:]
for r being Element of 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 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,Y0:] ;
thus I . (r * v) = I0 . (r * v0)
.= r * (I0 . v0) by P1
.= r * (I . v) by XX ; :: thesis: verum

end;

thus 0. (product <*X,Y*>) = I . (0. [:X,Y:]) by P1, XX; :: 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
PP1: v = [x1,y1] by LM01;
consider v1 being Element of REAL 2 such that
PP2: ( v1 = <*||.x1.||,||.y1.||*> & (prod_NORM (X,Y)) . (x1,y1) = |.v1.| ) by defNORM;
P55: I . v = I . (x1,y1) by PP1
.= <*x1,y1*> by P1 ;
reconsider Iv = I . v as Element of product (carr <*X,Y*>) by XX;
P58: ( <*x1,y1*> . 1 = x1 & <*x1,y1*> . 2 = y1 ) by FINSEQ_1:61;
( 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:4, FINSEQ_3:29;
X2: (normsequence (<*X,Y*>,Iv)) . j1 = the normF of (<*X,Y*> . j1) . (Iv . j1) by PRVECT_2:def 11
.= ||.x1.|| by P55, P58, FINSEQ_1:61 ;
X3: (normsequence (<*X,Y*>,Iv)) . j2 = the normF of (<*X,Y*> . j2) . (Iv . j2) by PRVECT_2:def 11
.= ||.y1.|| by P55, P58, FINSEQ_1:61 ;
len (normsequence (<*X,Y*>,Iv)) = len <*X,Y*> by PRVECT_2:def 11
.= 2 by FINSEQ_1:61 ;
then normsequence (<*X,Y*>,Iv) = v1 by PP2, X2, X3, FINSEQ_1:61;
hence ||.(I . v).|| = ||.v.|| by PP2, PP1, XX, PRVECT_2:def 12; :: thesis: verum

end;

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