let n be Nat; :: thesis: ( n < 2 implies for p being Element of Permutations n holds
( p is even & p = idseq n ) )
assume A1: n < 2 ; :: thesis: for p being Element of Permutations n holds
( p is even & p = idseq n )
let p be Element of Permutations n; :: thesis: ( p is even & p = idseq n )
reconsider P = p as Permutation of (Seg n) by MATRIX_1:def 12;

now :: thesis: ( p is even & p = idseq n )

per cases ( n = 0 or n = 1 ) by A1, NAT_1:23;

suppose A2: n = 0 ; :: thesis: ( p is even & p = idseq n )

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: verum

end;

suppose A5: n = 1 ; :: thesis: ( p is even & p = idseq n )

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: verum

end;

end;

end;

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