let V be RealLinearSpace; :: thesis: for F being Subset-Family of V st union F is finite holds
(center_of_mass V) .: F c= conv (union F)
let F be Subset-Family of V; :: thesis: ( union F is finite implies (center_of_mass V) .: F c= conv (union F) )
set B = center_of_mass V;
assume A1: union F is finite ; :: thesis: (center_of_mass V) .: F c= conv (union F)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (center_of_mass V) .: F or y in conv (union F) )
assume y in (center_of_mass V) .: F ; :: thesis: y in conv (union F)
then consider x being object such that
A2: x in dom (center_of_mass V) and
A3: x in F and
A4: (center_of_mass V) . x = y by FUNCT_1:def 6;
reconsider x = x as non empty Subset of V by A2, ZFMISC_1:56;
x c= union F by A3, ZFMISC_1:74;
then A5: y in conv x by A1, A4, Th16;
conv x c= conv (union F) by A3, RLTOPSP1:20, ZFMISC_1:74;
hence y in conv (union F) by A5; :: thesis: verum