let g, h be Function of (pi_1 (S,s)),(pi_1 (T,(f . s))); ( ( 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)) )
; g = h
now for x being Element of (pi_1 (S,s)) holds g . x = h . xlet x be
Element of
(pi_1 (S,s));
g . x = h . xconsider 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;
verum end;
hence
g = h
; verum