consider I being Function of [:X,Y:],(product <*X,Y*>) such that
A1:
( 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:])
by PRVECT_3:12;
reconsider I = I as LinearOperator of [:X,Y:],(product <*X,Y*>) by A3, A4, VECTSP_1:def 20, LOPBAN_1:def 5;
for a being Element of X
for b being Element of Y holds I . (a,b) = (IsoCPRLSP (X,Y)) . (a,b)
by defISO, A2;
hence
IsoCPRLSP (X,Y) is bijective
by A1, BINOP_1:2; verum