let V be RealLinearSpace; :: thesis: for If being finite affinely-independent Subset of V holds
( (center_of_mass V) . If in If iff card If = 1 )
let If be finite affinely-independent Subset of V; :: thesis: ( (center_of_mass V) . If in If iff card If = 1 )
set B = center_of_mass V;
hereby :: thesis: ( card If = 1 implies (center_of_mass V) . If in If )
assume A1: (center_of_mass V) . If in If ; :: thesis: 1 = card If
then reconsider BA = (center_of_mass V) . If as Element of V ;
(center_of_mass V) . If in conv If by A1, Th16;
then 1 = (BA |-- If) . BA by A1, RLAFFIN1:72
.= 1 / (card If) by A1, Th18 ;
hence 1 = card If by XCMPLX_1:58; :: thesis: verum
end;
assume A2: card If = 1 ; :: thesis: (center_of_mass V) . If in If
then consider x being object such that
A3: {x} = If by CARD_2:42;
x in If by A3, TARSKI:def 1;
then reconsider x = x as Element of V ;
(center_of_mass V) . If = (1 / (card If)) * (Sum If) by A3, Def2
.= (1 / 1) * x by A2, A3, RLVECT_2:9
.= x by RLVECT_1:def 8 ;
hence (center_of_mass V) . If in If by A3, TARSKI:def 1; :: thesis: verum