let f1, f2 be Function of (pi_1 (T,x1)),(pi_1 (T,x0)); :: thesis: ( ( for Q being Loop of x1 holds f1 . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) ) & ( for Q being Loop of x1 holds f2 . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) ) implies f1 = f2 )
assume that
A9: for Q being Loop of x1 holds f1 . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) and
A10: for Q being Loop of x1 holds f2 . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) ; :: thesis: f1 = f2
for x being Element of (pi_1 (T,x1)) holds f1 . x = f2 . x
proof
let x be Element of (pi_1 (T,x1)); :: thesis: f1 . x = f2 . x
consider L being Loop of x1 such that
A11: x = Class ((EqRel (T,x1)),L) by Th47;
thus f1 . x = Class ((EqRel (T,x0)),((P + L) + (- P))) by A9, A11
.= f2 . x by A10, A11 ; :: thesis: verum
end;
hence f1 = f2 ; :: thesis: verum