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 Th48;
thus f1 . x = Class (EqRel T,x0),((P + L) + (- P)) by A9, A11
.= f2 . x by A10, A11 ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:113; :: thesis: verum