theorem :: JGRAPH_4:112

for sn being Real holds 0. (TOP-REAL 2) = (sn -FanMorphE) . (0. (TOP-REAL 2)) by Th82, JGRAPH_2:3;