set X = <*> A;
<*> A is disjoint_valued ;
hence ex b₁ being FinSequence of A st b₁ is disjoint_valued ; :: thesis: verum