let f, g be Function of (pi_1 [:S,T:],[s,t]),(product <*(pi_1 S,s),(pi_1 T,t)*>); :: thesis: ( ( for x being Point of (pi_1 [:S,T:],[s,t]) ex l being Loop of [s,t] st
( x = Class (EqRel [:S,T:],[s,t]),l & f . x = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> ) ) & ( for x being Point of (pi_1 [:S,T:],[s,t]) ex l being Loop of [s,t] st
( x = Class (EqRel [:S,T:],[s,t]),l & g . x = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> ) ) implies f = g )
assume that
A9: for x being Point of (pi_1 [:S,T:],[s,t]) ex l being Loop of [s,t] st
( x = Class (EqRel [:S,T:],[s,t]),l & f . x = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> ) and
A10: for x being Point of (pi_1 [:S,T:],[s,t]) ex l being Loop of [s,t] st
( x = Class (EqRel [:S,T:],[s,t]),l & g . x = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> ) ; :: thesis: f = g

now

let x be Point of (pi_1 [:S,T:],[s,t]); :: thesis: f . x = g . x
consider l1 being Loop of [s,t] such that
A11: x = Class (EqRel [:S,T:],[s,t]),l1 and
A12: f . x = <*(Class (EqRel S,s),(pr1 l1)),(Class (EqRel T,t),(pr2 l1))*> by A9;
consider l2 being Loop of [s,t] such that
A13: x = Class (EqRel [:S,T:],[s,t]),l2 and
A14: g . x = <*(Class (EqRel S,s),(pr1 l2)),(Class (EqRel T,t),(pr2 l2))*> by A10;
A15: l1,l2 are_homotopic by A11, A13, TOPALG_1:47;
then pr2 l1, pr2 l2 are_homotopic by Th20;
then A16: Class (EqRel T,t),(pr2 l1) = Class (EqRel T,t),(pr2 l2) by TOPALG_1:47;
pr1 l1, pr1 l2 are_homotopic by A15, Th19;
hence f . x = g . x by A12, A14, A16, TOPALG_1:47; :: thesis: verum

end;

hence f = g by FUNCT_2:113; :: thesis: verum