:: deftheorem defines is_extension_of MEASURE8:def 12 :
for X being set
for F being Field_Subset of X
for S being SigmaField of X
for m being Measure of F
for M being sigma_Measure of S holds
( M is_extension_of m iff for A being set st A in F holds
M . A = m . A );