let f, g be Function of (pi_1 ([:S,T:],[s,t])),(product <*(pi_1 (S,s)),(pi_1 (T,t))*>); ( ( 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)))*> )
; f = g
now for x being Point of (pi_1 ([:S,T:],[s,t])) holds f . x = g . xlet x be
Point of
(pi_1 ([:S,T:],[s,t]));
f . x = g . xconsider 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;
verum end;
hence
f = g
; verum