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