let X be RealLinearSpace; :: thesis: for x being Point of X holds ((IsoCPRLSP X) ") . <*x*> = x
set I = IsoCPRLSP X;
set J = (IsoCPRLSP X) " ;
A1: dom (IsoCPRLSP X) = the carrier of X by FUNCT_2:def 1;
for x being Point of X holds ((IsoCPRLSP X) ") . <*x*> = x

proof

let x be Point of X; :: thesis: ((IsoCPRLSP X) ") . <*x*> = x
A2: (IsoCPRLSP X) . x = <*x*> by Def1;
reconsider z = x as Point of X ;
thus ((IsoCPRLSP X) ") . <*x*> = x by A1, A2, FUNCT_1:34; :: thesis: verum

end;

hence for x being Point of X holds ((IsoCPRLSP X) ") . <*x*> = x ; :: thesis: verum