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:48;
reconsider lt = f * ls as Loop of f . s by A1, Th27;
reconsider y = Class (EqRel T,(f . s)),lt as Element of (pi_1 T,(f . s)) by TOPALG_1:48;
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