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

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