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 ; :: thesis: verum