let n be Nat; :: thesis:
let p be Element of Permutations n; :: thesis:
reconsider P = p as Permutation of (Seg n) by MATRIX_1:def 12;
assume A1: n < 2 ; :: thesis:

per cases by A1, NAT_1:23;

suppose A2: n = 0 ; :: thesis:

then A3: Seg n = {} ;
A4: len (Permutations n) = n by MATRIX_1:9;
P = {} by A2;
hence ( p is even & p = idseq n ) by A4, A3, MATRIX_1:16, RELAT_1:55; :: thesis:

end;

suppose A5: n = 1 ; :: thesis:

A6: len (Permutations n) = n by MATRIX_1:9;
P = id (Seg n) by A5, MATRIX_1:10, TARSKI:def 1;
hence ( p is even & p = idseq n ) by A6, MATRIX_1:16; :: thesis:

end;

end;

end;

hence ( p is even & p = idseq n ) ; :: thesis: