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;

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

( (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 A2:
card If = 1
; :: thesis: (center_of_mass V) . If in Ifassume 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;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

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