reconsider MSi = Si as SigmaField of X ;
consider f being disjoint_valued Function of NAT ,MSi;
reconsider f = f as SetSequence of by Th2;
take f ; :: thesis: f is disjoint_valued
thus f is disjoint_valued ; :: thesis: verum