let V be RealLinearSpace; :: thesis: for A being Subset of V

for If being finite affinely-independent Subset of V st A c= If & (center_of_mass V) . If in Affin A holds

If = A

let A be Subset of V; :: thesis: for If being finite affinely-independent Subset of V st A c= If & (center_of_mass V) . If in Affin A holds

If = A

let If be finite affinely-independent Subset of V; :: thesis: ( A c= If & (center_of_mass V) . If in Affin A implies If = A )

set B = center_of_mass V;

assume that

A1: A c= If and

A2: (center_of_mass V) . If in Affin A ; :: thesis: If = A

A3: ((center_of_mass V) . If) |-- If = ((center_of_mass V) . If) |-- A by A1, A2, RLAFFIN1:77;

reconsider i = If as finite set ;

assume If <> A ; :: thesis: contradiction

then not If c= A by A1;

then consider x being object such that

A4: x in If and

A5: not x in A ;

reconsider x = x as Element of V by A4;

A6: (((center_of_mass V) . If) |-- If) . x = 1 / (card i) by A4, Th18;

Carrier (((center_of_mass V) . If) |-- A) c= A by RLVECT_2:def 6;

then not x in Carrier (((center_of_mass V) . If) |-- A) by A5;

hence contradiction by A3, A4, A6; :: thesis: verum

for If being finite affinely-independent Subset of V st A c= If & (center_of_mass V) . If in Affin A holds

If = A

let A be Subset of V; :: thesis: for If being finite affinely-independent Subset of V st A c= If & (center_of_mass V) . If in Affin A holds

If = A

let If be finite affinely-independent Subset of V; :: thesis: ( A c= If & (center_of_mass V) . If in Affin A implies If = A )

set B = center_of_mass V;

assume that

A1: A c= If and

A2: (center_of_mass V) . If in Affin A ; :: thesis: If = A

A3: ((center_of_mass V) . If) |-- If = ((center_of_mass V) . If) |-- A by A1, A2, RLAFFIN1:77;

reconsider i = If as finite set ;

assume If <> A ; :: thesis: contradiction

then not If c= A by A1;

then consider x being object such that

A4: x in If and

A5: not x in A ;

reconsider x = x as Element of V by A4;

A6: (((center_of_mass V) . If) |-- If) . x = 1 / (card i) by A4, Th18;

Carrier (((center_of_mass V) . If) |-- A) c= A by RLVECT_2:def 6;

then not x in Carrier (((center_of_mass V) . If) |-- A) by A5;

hence contradiction by A3, A4, A6; :: thesis: verum