defpred S₁[ 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 S₁[x,y]

proof

let x be Element of INT ; :: thesis: ex y being Element of (pi_1 ((Tunit_circle 2),c[10])) st S₁[x,y]
reconsider y = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop x)) as Element of (pi_1 ((Tunit_circle 2),c[10])) by TOPALG_1:48;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

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 S₁[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 ; :: thesis: for n being Integer holds f . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n))
let n be Integer; :: thesis: 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; :: thesis: verum