theorem LM190: :: NDIFF_7:33

for X, Y being RealNormSpace
for z being Point of [:X,Y:] holds
( z `1 = (proj (In (1,(dom <*X,Y*>)))) . ((IsoCPNrSP (X,Y)) . z) & z `2 = (proj (In (2,(dom <*X,Y*>)))) . ((IsoCPNrSP (X,Y)) . z) )