let X, Y be RealLinearSpace; :: thesis: 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; :: thesis: for y being Point of Y holds ((IsoCPRLSP (X,Y)) ") . <*x,y*> = [x,y]
let y be Point of Y; :: thesis: ((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; :: thesis: verum