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_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 B2: Seg n = {} ;
A3: len (Permutations n) = n by MATRIX_2:20;
P = {} by A2, FINSEQ_1:4;
hence ( p is even & p = idseq n ) by A2, A3, FINSEQ_1:4, MATRIX_2:29, RELAT_1:81, B2; :: thesis: verum

end;

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

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

end;

end;

end;

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