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 ;
lsg,lsh are_homotopic by ;
then ltg,lth are_homotopic by ;
hence g . x = h . x by ; :: thesis: verum
end;
hence g = h ; :: thesis: verum