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
now let x be
Element of
(pi_1 S,s);
:: thesis: 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, Th27;
lsg,
lsh are_homotopic
by A6, A8, TOPALG_1:47;
then
ltg,
lth are_homotopic
by A1, Th28;
hence
g . x = h . x
by A7, A9, TOPALG_1:47;
:: thesis: verum end;
hence
g = h
by FUNCT_2:113; :: thesis: verum