ex F being ManySortedSet of st
( F is uncurrying & rng F c= Funcs [:X,Y:],Z ) by Th1;
hence ex b₁ being ManySortedSet of st b₁ is uncurrying ; :: thesis: verum