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;

( 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 )end;

hence
( p is even & p = idseq n )
; :: thesis: verumper cases
( n = 0 or n = 1 )
by A1, NAT_1:23;

end;

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;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

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;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