let g, h be Function of (pi_1 (S,s)),(pi_1 (T,(f . s))); :: thesis: ( ( for x being Element of (pi_1 (S,s)) ex ls being Loop of s st

( x = Class ((EqRel (S,s)),ls) & g . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ) & ( for x being Element of (pi_1 (S,s)) ex ls being Loop of s st

( x = Class ((EqRel (S,s)),ls) & h . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ) implies g = h )

assume that

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

( x = Class ((EqRel (S,s)),ls) & g . x = Class ((EqRel (T,(f . s))),(f * ls)) ) and

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

( x = Class ((EqRel (S,s)),ls) & h . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ; :: thesis: g = h

( x = Class ((EqRel (S,s)),ls) & g . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ) & ( for x being Element of (pi_1 (S,s)) ex ls being Loop of s st

( x = Class ((EqRel (S,s)),ls) & h . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ) implies g = h )

assume that

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

( x = Class ((EqRel (S,s)),ls) & g . x = Class ((EqRel (T,(f . s))),(f * ls)) ) and

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

( x = Class ((EqRel (S,s)),ls) & h . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ; :: thesis: g = h

now :: thesis: for x being Element of (pi_1 (S,s)) holds g . x = h . x

hence
g = h
; :: thesis: verumlet x be Element of (pi_1 (S,s)); :: thesis: g . x = h . x

consider lsg being Loop of s such that

A6: x = Class ((EqRel (S,s)),lsg) and

A7: g . x = Class ((EqRel (T,(f . s))),(f * lsg)) by A4;

consider lsh being Loop of s such that

A8: x = Class ((EqRel (S,s)),lsh) and

A9: h . x = Class ((EqRel (T,(f . s))),(f * lsh)) by A5;

reconsider ltg = f * lsg, lth = f * lsh as Loop of f . s by A1, Th26;

lsg,lsh are_homotopic by A6, A8, TOPALG_1:46;

then ltg,lth are_homotopic by A1, Th27;

hence g . x = h . x by A7, A9, TOPALG_1:46; :: thesis: verum

end;consider lsg being Loop of s such that

A6: x = Class ((EqRel (S,s)),lsg) and

A7: g . x = Class ((EqRel (T,(f . s))),(f * lsg)) by A4;

consider lsh being Loop of s such that

A8: x = Class ((EqRel (S,s)),lsh) and

A9: h . x = Class ((EqRel (T,(f . s))),(f * lsh)) by A5;

reconsider ltg = f * lsg, lth = f * lsh as Loop of f . s by A1, Th26;

lsg,lsh are_homotopic by A6, A8, TOPALG_1:46;

then ltg,lth are_homotopic by A1, Th27;

hence g . x = h . x by A7, A9, TOPALG_1:46; :: thesis: verum