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