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