defpred S1[ 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 S1[x,y]
proof
let x be Element of (pi_1 (S,s)); :: thesis: ex y being Element of (pi_1 (T,(f . s))) st S1[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 ;
reconsider y = Class ((EqRel (T,(f . s))),lt) as Element of (pi_1 (T,(f . s))) by TOPALG_1:47;
take y ; :: thesis: S1[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 S1[x,h . x] from hence ex b1 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) & b1 . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ; :: thesis: verum