theorem Th25: :: TOPALG_5:25

for i being Integer
for f being Path of R^1 0, R^1 i holds Ciso . i = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * f))