let n be Nat; :: thesis: for perm being Element of Permutations n st perm <> idseq n holds
( ex i being Nat st
( i in Seg n & perm . i > i ) & ex j being Nat st
( j in Seg n & perm . j < j ) )
let p be Element of Permutations n; :: thesis: ( p <> idseq n implies ( ex i being Nat st
( i in Seg n & p . i > i ) & ex j being Nat st
( j in Seg n & p . j < j ) ) )
assume A1: p <> idseq n ; :: thesis: ( ex i being Nat st
( i in Seg n & p . i > i ) & ex j being Nat st
( j in Seg n & p . j < j ) )
reconsider p9 = p as Permutation of (Seg n) by MATRIX_2:def 11;
dom p9 = Seg n by FUNCT_2:67;
then consider x being set such that
A2: x in Seg n and
A3: p . x <> x by A1, FUNCT_1:34;
consider i being Element of NAT such that
A4: i = x and
A5: 1 <= i and
A6: i <= n by A2;

now

per cases ( p . i > i or p . i < i ) by A3, A4, XXREAL_0:1;

suppose p . i > i ; :: thesis: ex j being Nat st
( j in Seg n & p . j > j )

hence ex j being Nat st
( j in Seg n & p . j > j ) by A2, A4; :: thesis: verum

end;

suppose A7: p . i < i ; :: thesis: ex j being Nat st
( j in Seg n & p . j > j )

then reconsider i1 = i - 1 as Nat by NAT_1:20;
thus ex j being Nat st
( j in Seg n & p . j > j ) :: thesis: verum

proof

reconsider pS = p9 .: (Seg i) as finite set ;
A8: dom p9 = Seg n by FUNCT_2:67;
Seg i c= Seg n by A6, FINSEQ_1:7;
then Seg i,pS are_equipotent by A8, CARD_1:60;
then A9: card (Seg i) = card pS by CARD_1:21;
assume A10: for j being Nat st j in Seg n holds
p . j <= j ; :: thesis: contradiction
p .: (Seg i) c= Seg i1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in p .: (Seg i) or x in Seg i1 )
assume x in p .: (Seg i) ; :: thesis: x in Seg i1
then consider y being set such that
A11: y in dom p9 and
A12: y in Seg i and
A13: p . y = x by FUNCT_1:def 12;
consider j being Element of NAT such that
A14: j = y and
1 <= j and
A15: j <= i by A12;

per cases ( j = i or j < i ) by A15, XXREAL_0:1;

suppose j = i ; :: thesis: x in Seg i1

then p . j < i1 + 1 by A7;
then A16: p . j <= i1 by NAT_1:13;
A17: rng p9 = Seg n by FUNCT_2:def 3;
p . j in rng p by A11, A14, FUNCT_1:def 5;
then p . j >= 1 by A17, FINSEQ_1:3;
hence x in Seg i1 by A13, A14, A16, FINSEQ_1:3; :: thesis: verum

end;

suppose A18: j < i ; :: thesis: x in Seg i1

p . j <= j by A10, A11, A14;
then p . j < i1 + 1 by A18, XXREAL_0:2;
then A19: p . j <= i1 by NAT_1:13;
A20: rng p9 = Seg n by FUNCT_2:def 3;
p . j in rng p by A11, A14, FUNCT_1:def 5;
then p . j >= 1 by A20, FINSEQ_1:3;
hence x in Seg i1 by A13, A14, A19, FINSEQ_1:3; :: thesis: verum

end;

end;

end;

then A21: card pS <= card (Seg i1) by NAT_1:44;
card (Seg i) = i by FINSEQ_1:78;
then i1 + 1 <= i1 by A9, A21, FINSEQ_1:78;
hence contradiction by NAT_1:13; :: thesis: verum

end;

end;

end;

end;

hence ex j being Nat st
( j in Seg n & p . j > j ) ; :: thesis: ex j being Nat st
( j in Seg n & p . j < j )
A22: n in NAT by ORDINAL1:def 13;

per cases ( p . i < i or p . i > i ) by A3, A4, XXREAL_0:1;

suppose p . i < i ; :: thesis: ex j being Nat st
( j in Seg n & p . j < j )

hence ex j being Nat st
( j in Seg n & p . j < j ) by A2, A4; :: thesis: verum

end;

suppose A23: p . i > i ; :: thesis: ex j being Nat st
( j in Seg n & p . j < j )

thus ex j being Nat st
( j in Seg n & p . j < j ) :: thesis: verum

proof

set NI = nat_interval i,n;
reconsider pN = p9 .: (nat_interval i,n) as finite set ;
A24: i in nat_interval i,n by A22, A6, SGRAPH1:3;
assume A25: for j being Nat st j in Seg n holds
p . j >= j ; :: thesis: contradiction
A26: pN c= nat_interval i,n

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in pN or x in nat_interval i,n )
A27: rng p9 = Seg n by FUNCT_2:def 3;
assume x in pN ; :: thesis: x in nat_interval i,n
then consider j being set such that
A28: j in dom p9 and
A29: j in nat_interval i,n and
A30: p . j = x by FUNCT_1:def 12;
reconsider j = j as Nat by A29;
reconsider pj = p . j as Element of NAT by ORDINAL1:def 13;
A31: j <= pj by A25, A28;
i <= j by A22, A29, SGRAPH1:3;
then A32: i <= pj by A31, XXREAL_0:2;
pj in rng p9 by A28, FUNCT_1:def 5;
then pj <= n by A27, FINSEQ_1:3;
hence x in nat_interval i,n by A22, A30, A32, SGRAPH1:2; :: thesis: verum

end;

dom p9 = Seg n by FUNCT_2:67;
then nat_interval i,n,pN are_equipotent by A22, A5, CARD_1:60, SGRAPH1:5;
then card (nat_interval i,n) = card pN by CARD_1:21;
then nat_interval i,n = pN by A26, CARD_FIN:1;
then consider j being set such that
A33: j in dom p9 and
A34: j in nat_interval i,n and
A35: p . j = i by A24, FUNCT_1:def 12;
reconsider j = j as Nat by A34;
A36: i <= j by A22, A34, SGRAPH1:3;
j <= i by A25, A33, A35;
hence contradiction by A23, A35, A36, XXREAL_0:1; :: thesis: verum

end;

end;

end;