theorem Th27: :: MEASURE9:29

for p being ext-real number
for M being Matrix of ExtREAL st ( for i being Nat st i in dom M holds
not p in rng (M . i) ) holds
for j being Nat st j in dom (M @) holds
not p in rng ((M @) . j)