let m be Element of M; :: thesis: ( m is Function-like & m is Relation-like )
m is multiset of I by Th2;
hence ( m is Function-like & m is Relation-like ) ; :: thesis: verum