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 :: thesis: for x being Element of (pi_1 (S,s)) holds g . x = h . x

let 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;

hence g = h ; :: thesis: verum