theorem Th7: :: MESFUN12:7

for X being non empty set
for A1, A2 being Subset of X
for r1, r2 being Real holds <*(chi (r1,A1,X)),(chi (r2,A2,X))*> is summable FinSequence of Funcs (X,ExtREAL)