defpred S₁[ set , set ] means ex ls being Loop of s st
( $1 = Class ((EqRel (S,s)),ls) & $2 = Class ((EqRel (T,(f . s))),(f * ls)) );
A2: for x being Element of (pi_1 (S,s)) ex y being Element of (pi_1 (T,(f . s))) st S₁[x,y]

proof

let x be Element of (pi_1 (S,s)); :: thesis: ex y being Element of (pi_1 (T,(f . s))) st S₁[x,y]
consider ls being Loop of s such that
A3: x = Class ((EqRel (S,s)),ls) by TOPALG_1:47;
reconsider lt = f * ls as Loop of f . s by A1, Th26;
reconsider y = Class ((EqRel (T,(f . s))),lt) as Element of (pi_1 (T,(f . s))) by TOPALG_1:47;
take y ; :: thesis: S₁[x,y]
take ls ; :: thesis: ( x = Class ((EqRel (S,s)),ls) & y = Class ((EqRel (T,(f . s))),(f * ls)) )
thus ( x = Class ((EqRel (S,s)),ls) & y = Class ((EqRel (T,(f . s))),(f * ls)) ) by A3; :: thesis: verum

end;

ex h being Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) st
for x being Element of (pi_1 (S,s)) holds S₁[x,h . x] from FUNCT_2:sch 3(A2);
hence ex b₁ being Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) st
for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & b₁ . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ; :: thesis: verum