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

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

hence
f = g
; :: thesis: verum
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;thus f . x = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop x)) by A3

.= g . x by A4 ; :: thesis: verum