for Omega being non empty finite set
for f being PartFunc of Omega,REAL holds
( f is_simple_func_in Trivial-SigmaField Omega & dom f is Element of Trivial-SigmaField Omega )