let m be Element of M; :: thesis: ( m is I -defined & m is natural-valued & m is finite-support )
m is multiset of I by Th2;
hence ( m is I -defined & m is natural-valued & m is finite-support ) ; :: thesis: verum