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