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