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 that
A1:
(T_1-reflect S) * f = g1 * (T_1-reflect T)
and
A2:
(T_1-reflect S) * f = g2 * (T_1-reflect T)
; :: thesis: g1 = g2
A3:
( dom g1 = the carrier of (T_1-reflex T) & dom g2 = the carrier of (T_1-reflex T) )
by FUNCT_2:def 1;
now let x be
set ;
:: thesis: ( x in dom g1 implies g2 . x = g1 . x )assume A4:
x in dom g1
;
:: thesis: g2 . x = g1 . xthen A5:
x in the
carrier of
(T_1-reflex T)
;
A6:
the
carrier of
(T_1-reflex T) = Intersection (Closed_Partitions T)
by BORSUK_1:def 10;
then consider y being
Element of
T such that A7:
x = EqClass y,
(Intersection (Closed_Partitions T))
by A4, EQREL_1:51;
A8:
(
dom (T_1-reflect T) = the
carrier of
T &
rng (T_1-reflect T) c= the
carrier of
(T_1-reflex T) )
by FUNCT_2:def 1;
reconsider y =
y as
Element of
T ;
T_1-reflect T = proj (Intersection (Closed_Partitions T))
by BORSUK_1:def 11;
then A9:
(
y in (T_1-reflect T) . y &
y in x )
by A7, BORSUK_1:def 1, EQREL_1:def 8;
set ty =
(T_1-reflect T) . y;
(T_1-reflect T) . y in Intersection (Closed_Partitions T)
by A6;
then A10:
(
(T_1-reflect T) . y misses x or
(T_1-reflect T) . y = x )
by A5, A6, EQREL_1:def 6;
hence g2 . x =
(g2 * (T_1-reflect T)) . y
by A8, A9, FUNCT_1:23, XBOOLE_0:3
.=
g1 . x
by A1, A2, A8, A9, A10, FUNCT_1:23, XBOOLE_0:3
;
:: thesis: verum end;
hence
g1 = g2
by A3, FUNCT_1:9; :: thesis: verum