let f, g be Function of INT.Group ,(pi_1 (Tunit_circle 2),c[10] ); :: thesis: ( ( for n being Integer holds f . n = Class (EqRel (Tunit_circle 2),c[10] ),(cLoop n) ) & ( for n being Integer holds g . n = Class (EqRel (Tunit_circle 2),c[10] ),(cLoop n) ) implies f = g )
assume that
A3: for n being Integer holds f . n = Class (EqRel (Tunit_circle 2),c[10] ),(cLoop n) and
A4: for n being Integer holds g . n = Class (EqRel (Tunit_circle 2),c[10] ),(cLoop n) ; :: thesis: f = g
for x being Element of INT.Group holds f . x = g . x

proof

let x be Element of INT.Group ; :: thesis: f . x = g . x
thus f . x = Class (EqRel (Tunit_circle 2),c[10] ),(cLoop x) by A3
.= g . x by A4 ; :: thesis: verum

end;

hence f = g by FUNCT_2:113; :: thesis: verum