theorem LM180: :: NDIFF_7:32

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