now :: thesis: 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 = x2

set B = center_of_mass V;
set T = the topology of Kas;
let x1, x2 be object ; :: thesis: ( 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 ; :: thesis: x1 = x2
A4: ( ((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; :: thesis: verum

end;

hence (center_of_mass V) | the topology of Kas is one-to-one by FUNCT_1:def 4; :: thesis: verum