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));
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 A1, Th26;
reconsider y =
Class (
(EqRel (T,(f . s))),
lt) as
Element of
(pi_1 (T,(f . s))) by TOPALG_1:47;
take
y
;
S1[x,y]
take
ls
;
( 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;
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 FUNCT_2:sch 3(A2);
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)) )
; verum