let g1, g2 be continuous Function of (T_1-reflex T),(T_1-reflex S); :: thesis: ( (T_1-reflect S) * f = g1 * (T_1-reflect T) & (T_1-reflect S) * f = g2 * (T_1-reflect T) implies g1 = g2 )
assume A1: ( (T_1-reflect S) * f = g1 * (T_1-reflect T) & (T_1-reflect S) * f = g2 * (T_1-reflect T) ) ; :: thesis: g1 = g2

A2: now :: thesis: for x being object st x in dom g1 holds
g2 . x = g1 . x

let x be object ; :: thesis: ( x in dom g1 implies g2 . x = g1 . x )
assume A3: x in dom g1 ; :: thesis: g2 . x = g1 . x
then A4: x in the carrier of (T_1-reflex T) ;
A5: the carrier of (T_1-reflex T) = Intersection (Closed_Partitions T) by BORSUK_1:def 7;
then consider y being Element of T such that
A6: x = EqClass (y,(Intersection (Closed_Partitions T))) by A3, EQREL_1:42;
reconsider y = y as Element of T ;
set ty = (T_1-reflect T) . y;
reconsider xx = x as set by TARSKI:1;
(T_1-reflect T) . y in Intersection (Closed_Partitions T) by A5;
then A7: ( (T_1-reflect T) . y misses xx or (T_1-reflect T) . y = x ) by A4, A5, EQREL_1:def 4;
T_1-reflect T = proj (Intersection (Closed_Partitions T)) by BORSUK_1:def 8;
then A8: ( dom (T_1-reflect T) = the carrier of T & y in (T_1-reflect T) . y ) by EQREL_1:def 9, FUNCT_2:def 1;
A9: y in xx by A6, EQREL_1:def 6;
hence g2 . x = (g2 * (T_1-reflect T)) . y by A8, A7, FUNCT_1:13, XBOOLE_0:3
.= g1 . x by A1, A8, A9, A7, FUNCT_1:13, XBOOLE_0:3 ;
:: thesis: verum

end;

( dom g1 = the carrier of (T_1-reflex T) & dom g2 = the carrier of (T_1-reflex T) ) by FUNCT_2:def 1;
hence g1 = g2 by A2, FUNCT_1:2; :: thesis: verum