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