theorem defISOA1: :: NDIFF_7:18

for X, Y being RealNormSpace
for x being Point of X
for y being Point of Y holds ((IsoCPNrSP (X,Y)) ") . <*x,y*> = [x,y]