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

now

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

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

then dom P = {} ;
then ( P = {} & len (Permutations n) = n ) by MATRIX_2:20;
hence ( p is even & p = idseq n ) by A2, FINSEQ_1:4, MATRIX_2:29, RELAT_1:81; :: thesis: verum

end;

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

then ( P = id (Seg n) & len (Permutations n) = n ) by MATRIX_2:20, MATRIX_2:21, TARSKI:def 1;
hence ( p is even & p = idseq n ) by MATRIX_2:29; :: thesis: verum

end;

end;

end;

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