let X, Y be RealNormSpace; 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;
for y being Point of Y holds ((IsoCPNrSP (X,Y)) ") . <*x,y*> = [x,y]let y be
Point of
Y;
((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;
verum
end;
hence
for x being Point of X
for y being Point of Y holds ((IsoCPNrSP (X,Y)) ") . <*x,y*> = [x,y]
; verum