let g1, g2 be continuous Function of (T_1-reflex T),(T_1-reflex S); ( (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) )
; g1 = g2
A2:
now for x being object st x in dom g1 holds
g2 . x = g1 . xlet x be
object ;
( x in dom g1 implies g2 . x = g1 . x )assume A3:
x in dom g1
;
g2 . x = g1 . xthen 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
;
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; verum