defpred S1[ Integer, set ] means $2 = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop $1));
A1:
for x being Element of INT ex y being Element of (pi_1 ((Tunit_circle 2),c[10])) st S1[x,y]
consider f being Function of INT, the carrier of (pi_1 ((Tunit_circle 2),c[10])) such that
A2:
for x being Element of INT holds S1[x,f . x]
from FUNCT_2:sch 3(A1);
reconsider f = f as Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) ;
take
f
; for n being Integer holds f . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n))
let n be Integer; f . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n))
n in INT
by INT_1:def 2;
hence
f . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n))
by A2; verum