let X, Y be RealLinearSpace; 0. (product <*X,Y*>) = (IsoCPRLSP (X,Y)) . (0. [:X,Y:])
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
A4:
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;
for a being Element of X
for b being Element of Y holds I . (a,b) = (IsoCPRLSP (X,Y)) . (a,b)
by A1, defISO;
hence
0. (product <*X,Y*>) = (IsoCPRLSP (X,Y)) . (0. [:X,Y:])
by A4, BINOP_1:2; verum