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:12;
A3: for x being Element of (pi_1 (T,x1)) ex y being Element of (pi_1 (T,x0)) st S₁[x,y]

proof

let x be Element of (pi_1 (T,x1)); :: thesis: ex y being Element of (pi_1 (T,x0)) st S₁[x,y]
consider Q being Loop of x1 such that
A4: x = Class ((EqRel (T,x1)),Q) by Th47;
reconsider y = Class ((EqRel (T,x0)),((P + Q) + (- P))) as Element of (pi_1 (T,x0)) by Th47;
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 (pi_1 (T,x1)) 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 (pi_1 (T,x1)) by EQREL_1:def 3;
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:12;
L,Q are_homotopic by A6, Th46;
then P + L,P + Q are_homotopic by A1, A2, BORSUK_6:75;
then (P + L) + (- P),(P + Q) + (- P) are_homotopic by A1, A8, BORSUK_6:75;
hence f . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) by A7, Th46; :: thesis: verum