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 :: thesis: for x being Point of (pi_1 ([:S,T:],[s,t])) holds f . x = g . x

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:46;
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:46;
pr1 l1, pr1 l2 are_homotopic by A15, Th19;
hence f . x = g . x by A12, A14, A16, TOPALG_1:46; :: thesis: verum

end;

hence f = g ; :: thesis: verum