theorem :: JGRAPH_4:143

for a being Real holds 0. (TOP-REAL 2) = (a -FanMorphS) . (0. (TOP-REAL 2)) by Th113, JGRAPH_2:3;