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 X -measurable )
let f be PartFunc of Omega,REAL; :: thesis: ex X being Element of Trivial-SigmaField Omega st
( dom f = X & f is X -measurable )
set Sigma = Trivial-SigmaField Omega;
reconsider X = dom f as Element of Trivial-SigmaField Omega ;
take X ; :: thesis: ( dom f = X & f is X -measurable )
thus ( dom f = X & f is X -measurable ) by Th6, MESFUNC6:50; :: thesis: verum