theorem defISOA1: :: LOPBAN12:5

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