reconsider MSi = Si as SigmaField of X ;
set f = the disjoint_valued sequence of MSi;
reconsider f = the disjoint_valued sequence of MSi as SetSequence of Si by Th2;
take f ; :: thesis: f is V125()
thus f is V125() ; :: thesis: verum