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