consider I being Function of [:X,Y:],(product <*X,Y*>) such that
( I is one-to-one & I is onto ) and
A2: for x being Point of X
for y being Point of Y holds I . (x,y) = <*x,y*> and
A3: for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) and
A4: for v being Point of [:X,Y:]
for r being Real holds I . (r * v) = r * (I . v) and
0. (product <*X,Y*>) = I . (0. [:X,Y:]) and
for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| by PRVECT_3:15;
reconsider I = I as LinearOperator of [:X,Y:],(product <*X,Y*>) by A3, A4, VECTSP_1:def 20, LOPBAN_1:def 5;
take I ; :: thesis: for x being Point of X
for y being Point of Y holds I . (x,y) = <*x,y*>
thus for x being Point of X
for y being Point of Y holds I . (x,y) = <*x,y*> by A2; :: thesis: verum