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