let Omega be non empty finite set ; :: thesis: for f being PartFunc of Omega,REAL ex X being Element of Trivial-SigmaField Omega st
( dom f = X & f is_measurable_on X )
let f be PartFunc of Omega,REAL ; :: thesis: ex X being Element of Trivial-SigmaField Omega st
( dom f = X & f is_measurable_on X )
set Sigma = Trivial-SigmaField Omega;
reconsider X = dom f as Element of Trivial-SigmaField Omega ;
take X ; :: thesis: ( dom f = X & f is_measurable_on X )
thus ( dom f = X & f is_measurable_on X ) by Lm6, MESFUNC6:50; :: thesis: verum