let X, Y be RealNormSpace; :: thesis: for x being Point of X
for y being Point of Y holds ((IsoCPNrSP (X,Y)) ") . <*x,y*> = [x,y]
set I = IsoCPNrSP (X,Y);
set J = (IsoCPNrSP (X,Y)) " ;
P0: dom (IsoCPNrSP (X,Y)) = the carrier of [:X,Y:] by FUNCT_2:def 1;
for x being Point of X
for y being Point of Y holds ((IsoCPNrSP (X,Y)) ") . <*x,y*> = [x,y]

proof

let x be Point of X; :: thesis: for y being Point of Y holds ((IsoCPNrSP (X,Y)) ") . <*x,y*> = [x,y]
let y be Point of Y; :: thesis: ((IsoCPNrSP (X,Y)) ") . <*x,y*> = [x,y]
Q1: (IsoCPNrSP (X,Y)) . (x,y) = <*x,y*> by defISO;
reconsider z = [x,y] as Point of [:X,Y:] ;
((IsoCPNrSP (X,Y)) ") . ((IsoCPNrSP (X,Y)) . z) = z by P0, FUNCT_1:34;
hence ((IsoCPNrSP (X,Y)) ") . <*x,y*> = [x,y] by Q1; :: thesis: verum

end;

hence for x being Point of X
for y being Point of Y holds ((IsoCPNrSP (X,Y)) ") . <*x,y*> = [x,y] ; :: thesis: verum