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

hence
(center_of_mass V) | the topology of Kas is one-to-one
by FUNCT_1:def 4; :: thesis: verumx1 = 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;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