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:47;
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:46;
then f * ls,f * ls1 are_homotopic by Th27;
hence (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = Class ((EqRel (T,(f . s))),(f * ls)) by A2, TOPALG_1:46; :: thesis: verum