now for x1, x2 being object st x1 in dom ((center_of_mass V) | the topology of Kas) & x2 in dom ((center_of_mass V) | the topology of Kas) & ((center_of_mass V) | the topology of Kas) . x1 = ((center_of_mass V) | the topology of Kas) . x2 holds
x1 = x2set B =
center_of_mass V;
set T = the
topology of
Kas;
let x1,
x2 be
object ;
( x1 in dom ((center_of_mass V) | the topology of Kas) & x2 in dom ((center_of_mass V) | the topology of Kas) & ((center_of_mass V) | the topology of Kas) . x1 = ((center_of_mass V) | the topology of Kas) . x2 implies x1 = x2 )set BT =
(center_of_mass V) | the
topology of
Kas;
assume that A1:
x1 in dom ((center_of_mass V) | the topology of Kas)
and A2:
x2 in dom ((center_of_mass V) | the topology of Kas)
and A3:
((center_of_mass V) | the topology of Kas) . x1 = ((center_of_mass V) | the topology of Kas) . x2
;
x1 = x2A4:
(
((center_of_mass V) | the topology of Kas) . x1 = (center_of_mass V) . x1 &
((center_of_mass V) | the topology of Kas) . x2 = (center_of_mass V) . x2 )
by A1, A2, FUNCT_1:47;
dom ((center_of_mass V) | the topology of Kas) = (dom (center_of_mass V)) /\ the
topology of
Kas
by RELAT_1:61;
then
(
x1 in the
topology of
Kas &
x2 in the
topology of
Kas )
by A1, A2, XBOOLE_0:def 4;
then reconsider A1 =
x1,
A2 =
x2 as
Simplex of
Kas by PRE_TOPC:def 2;
not
A1 is
empty
by A1, ZFMISC_1:56;
then A5:
(center_of_mass V) . A1 in conv (@ A1)
by RLAFFIN2:16;
not
A2 is
empty
by A2, ZFMISC_1:56;
then
(center_of_mass V) . A2 in conv (@ A2)
by RLAFFIN2:16;
then A6:
(center_of_mass V) . A1 in (conv (@ A1)) /\ (conv (@ A2))
by A3, A4, A5, XBOOLE_0:def 4;
A7:
(
(conv (@ A1)) /\ (conv (@ A2)) = conv (@ (A1 /\ A2)) &
conv (@ (A1 /\ A2)) c= Affin (@ (A1 /\ A2)) )
by Def8, RLAFFIN1:65;
then
A1 /\ A2 = A1
by A6, RLAFFIN2:21, XBOOLE_1:17;
hence
x1 = x2
by A3, A4, A6, A7, RLAFFIN2:21, XBOOLE_1:17;
verum end;
hence
(center_of_mass V) | the topology of Kas is one-to-one
by FUNCT_1:def 4; verum