2 const 0 is 2 -ary ;
hence ex b₁ being NAT * -defined homogeneous Function st
( not b₁ is empty & b₁ is 2 -ary & b₁ is len-total & b₁ is to-naturals ) ; :: thesis: verum