theorem Th14: :: MESFUN12:14

for X being set
for A1, A2 being Subset of X
for er being ExtReal holds (chi (er,A1,X)) | A2 = (chi (er,(A1 /\ A2),X)) | A2