defpred S₁[ set , set ] means ex L being Loop of x1 st
( $1 = Class (EqRel T,x1),L & $2 = Class (EqRel T,x0),((P + L) + (- P)) );
A2: P,P are_homotopic by A1, BORSUK_2:15;
A3: for x being Element of ex y being Element of st S₁[x,y]

proof

let x be Element of ; :: thesis: ex y being Element of st S₁[x,y]
consider Q being Loop of x1 such that
A4: x = Class (EqRel T,x1),Q by Th48;
reconsider y = Class (EqRel T,x0),((P + Q) + (- P)) as Element of by Th48;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by A4; :: thesis: verum

end;

consider f being Function of the carrier of (pi_1 T,x1),the carrier of (pi_1 T,x0) such that
A5: for x being Element of holds S₁[x,f . x] from FUNCT_2:sch 3(A3);
reconsider f = f as Function of (pi_1 T,x1),(pi_1 T,x0) ;
take f ; :: thesis: for Q being Loop of x1 holds f . (Class (EqRel T,x1),Q) = Class (EqRel T,x0),((P + Q) + (- P))
let Q be Loop of x1; :: thesis: f . (Class (EqRel T,x1),Q) = Class (EqRel T,x0),((P + Q) + (- P))
( the carrier of (pi_1 T,x1) = Class (EqRel T,x1) & Q in Loops x1 ) by Def1, Def5;
then Class (EqRel T,x1),Q is Element of by EQREL_1:def 5;
then consider L being Loop of x1 such that
A6: Class (EqRel T,x1),Q = Class (EqRel T,x1),L and
A7: f . (Class (EqRel T,x1),Q) = Class (EqRel T,x0),((P + L) + (- P)) by A5;
A8: - P, - P are_homotopic by A1, BORSUK_2:15;
L,Q are_homotopic by A6, Th47;
then P + L,P + Q are_homotopic by A1, A2, BORSUK_6:83;
then (P + L) + (- P),(P + Q) + (- P) are_homotopic by A1, A8, BORSUK_6:83;
hence f . (Class (EqRel T,x1),Q) = Class (EqRel T,x0),((P + Q) + (- P)) by A7, Th47; :: thesis: verum