let X, Y be RealLinearSpace; for x being Point of X
for y being Point of Y holds ((IsoCPRLSP (X,Y)) ") . <*x,y*> = [x,y]
set I = IsoCPRLSP (X,Y);
set J = (IsoCPRLSP (X,Y)) " ;
A1:
dom (IsoCPRLSP (X,Y)) = the carrier of [:X,Y:]
by FUNCT_2:def 1;
let x be Point of X; for y being Point of Y holds ((IsoCPRLSP (X,Y)) ") . <*x,y*> = [x,y]
let y be Point of Y; ((IsoCPRLSP (X,Y)) ") . <*x,y*> = [x,y]
A2:
(IsoCPRLSP (X,Y)) . (x,y) = <*x,y*>
by defISO;
reconsider z = [x,y] as Point of [:X,Y:] ;
((IsoCPRLSP (X,Y)) ") . ((IsoCPRLSP (X,Y)) . z) = z
by A1, FUNCT_1:34;
hence
((IsoCPRLSP (X,Y)) ") . <*x,y*> = [x,y]
by A2; verum