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

hence g1 = g2 by A2, FUNCT_1:2; :: thesis: verum

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

( dom g1 = the carrier of (T_1-reflex T) & dom g2 = the carrier of (T_1-reflex T) )
by FUNCT_2:def 1;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;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

hence g1 = g2 by A2, FUNCT_1:2; :: thesis: verum