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
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 & f . x = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> ) and
A11: 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
A12: x = Class (EqRel [:S,T:],[s,t]),l1 and
A13: f . x = <*(Class (EqRel S,s),(pr1 l1)),(Class (EqRel T,t),(pr2 l1))*> by A10;
consider l2 being Loop of [s,t] such that
A14: x = Class (EqRel [:S,T:],[s,t]),l2 and
A15: g . x = <*(Class (EqRel S,s),(pr1 l2)),(Class (EqRel T,t),(pr2 l2))*> by A11;
A16: l1,l2 are_homotopic by A12, A14, TOPALG_1:47;
then A17: pr1 l1, pr1 l2 are_homotopic by Th19;
pr2 l1, pr2 l2 are_homotopic by A16, Th20;
then Class (EqRel T,t),(pr2 l1) = Class (EqRel T,t),(pr2 l2) by TOPALG_1:47;
hence f . x = g . x by A13, A15, A17, TOPALG_1:47; :: thesis: verum

end;

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