let S, T be non empty TopSpace; :: thesis: for s being Point of S
for f being continuous Function of S,T
for ls being Loop of s holds (FundGrIso f,s) . (Class (EqRel S,s),ls) = Class (EqRel T,(f . s)),(f * ls)
let s be Point of S; :: thesis: for f being continuous Function of S,T
for ls being Loop of s holds (FundGrIso f,s) . (Class (EqRel S,s),ls) = Class (EqRel T,(f . s)),(f * ls)
let f be continuous Function of S,T; :: thesis: for ls being Loop of s holds (FundGrIso f,s) . (Class (EqRel S,s),ls) = Class (EqRel T,(f . s)),(f * ls)
let ls be Loop of s; :: thesis: (FundGrIso f,s) . (Class (EqRel S,s),ls) = Class (EqRel T,(f . s)),(f * ls)
reconsider x = Class (EqRel S,s),ls as Element of (pi_1 S,s) by TOPALG_1:48;
consider ls1 being Loop of s such that
A1: x = Class (EqRel S,s),ls1 and
A2: (FundGrIso f,s) . x = Class (EqRel T,(f . s)),(f * ls1) by Def1;
ls,ls1 are_homotopic by A1, TOPALG_1:47;
then f * ls,f * ls1 are_homotopic by Th28;
hence (FundGrIso f,s) . (Class (EqRel S,s),ls) = Class (EqRel T,(f . s)),(f * ls) by A2, TOPALG_1:47; :: thesis: verum