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 V118()
thus f is V118() ; :: thesis: verum