defpred S_{1}[ 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_{1}[x,y]

for x being Element of (pi_1 (S,s)) holds S_{1}[x,h . x]
from FUNCT_2:sch 3(A2);

hence ex b_{1} 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_{1} . x = Class ((EqRel (T,(f . s))),(f * ls)) )
; :: thesis: verum

( $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

proof

ex h being Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) st
let x be Element of (pi_1 (S,s)); :: thesis: ex y being Element of (pi_1 (T,(f . s))) st S_{1}[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_{1}[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;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

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

for x being Element of (pi_1 (S,s)) holds S

hence ex b

for x being Element of (pi_1 (S,s)) ex ls being Loop of s st

( x = Class ((EqRel (S,s)),ls) & b