theorem Th97: :: JGRAPH_4:97

for sn being Real
for p being Point of (TOP-REAL 2) holds |.((sn -FanMorphE) . p).| = |.p.|