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