now :: thesis: for x1, x2 being object st x1 in dom (() | the topology of Kas) & x2 in dom (() | the topology of Kas) & (() | the topology of Kas) . x1 = (() | 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 (() | the topology of Kas) & x2 in dom (() | the topology of Kas) & (() | the topology of Kas) . x1 = (() | the topology of Kas) . x2 implies x1 = x2 )
set BT = () | the topology of Kas;
assume that
A1: x1 in dom (() | the topology of Kas) and
A2: x2 in dom (() | the topology of Kas) and
A3: ((center_of_mass V) | the topology of Kas) . x1 = (() | the topology of Kas) . x2 ; :: thesis: x1 = x2
A4: ( ((center_of_mass V) | the topology of Kas) . x1 = () . x1 & (() | the topology of Kas) . x2 = () . x2 ) by ;
dom (() | the topology of Kas) = () /\ the topology of Kas by RELAT_1:61;
then ( x1 in the topology of Kas & x2 in the topology of Kas ) by ;
then reconsider A1 = x1, A2 = x2 as Simplex of Kas by PRE_TOPC:def 2;
not A1 is empty by ;
then A5: (center_of_mass V) . A1 in conv (@ A1) by RLAFFIN2:16;
not A2 is empty by ;
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 ;
A7: ( (conv (@ A1)) /\ (conv (@ A2)) = conv (@ (A1 /\ A2)) & conv (@ (A1 /\ A2)) c= Affin (@ (A1 /\ A2)) ) by ;
then A1 /\ A2 = A1 by ;
hence x1 = x2 by ; :: thesis: verum
end;
hence (center_of_mass V) | the topology of Kas is one-to-one by FUNCT_1:def 4; :: thesis: verum