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: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: 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 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) )
; :: thesis: verum