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
A3: 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
A4: 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
A5: x = Class ((EqRel (S,s)),lsg) and
A6: g . x = Class ((EqRel (T,(f . s))),(f * lsg)) by A3;
consider lsh being Loop of s such that
A7: x = Class ((EqRel (S,s)),lsh) and
A8: h . x = Class ((EqRel (T,(f . s))),(f * lsh)) by A4;
reconsider ltg = f * lsg, lth = f * lsh as Loop of f . s by B1, Th26;
lsg,lsh are_homotopic by A5, A7, TOPALG_1:46;
then ltg,lth are_homotopic by B1, Th27;
hence g . x = h . x by A6, A8, TOPALG_1:46; :: thesis: verum

end;

hence g = h by FUNCT_2:63; :: thesis: verum