defpred S_{1}[ 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_{1}[x,y]

A2: for x being Element of INT holds S_{1}[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

A1: for x being Element of INT ex y being Element of (pi_1 ((Tunit_circle 2),c[10])) st S

proof

consider f being Function of INT, the carrier of (pi_1 ((Tunit_circle 2),c[10])) such that
let x be Element of INT ; :: thesis: ex y being Element of (pi_1 ((Tunit_circle 2),c[10])) st S_{1}[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:47;

take y ; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
; :: thesis: verum

end;reconsider y = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop x)) as Element of (pi_1 ((Tunit_circle 2),c[10])) by TOPALG_1:47;

take y ; :: thesis: S

thus S

A2: for x being Element of INT holds S

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