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

(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