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