reconsider f = id (Seg n) as Permutation of (Seg n) ;
f is even by MATRIX_1:16;
hence ex b₁ being Permutation of (Seg n) st b₁ is even ; :: thesis: verum