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 p' = p as Permutation of (Seg n) by MATRIX_2:def 11;
A2: n in NAT by ORDINAL1:def 13;
dom p' = Seg n by FUNCT_2:67;
then consider x being set such that
A3: ( x in Seg n & p . x <> x ) by A1, FUNCT_1:34;
consider i being Element of NAT such that
A4: ( i = x & 1 <= i & i <= n ) by A3;

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 A3, A4; :: thesis: verum

end;

suppose A5: 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

assume A6: for j being Nat st j in Seg n holds
p . j <= j ; :: thesis: contradiction
A7: 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
A8: ( y in dom p' & y in Seg i & p . y = x ) by FUNCT_1:def 12;
consider j being Element of NAT such that
A9: ( j = y & 1 <= j & j <= i ) by A8;

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

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

then ( p . j < i1 + 1 & p . j in rng p & rng p' = Seg n ) by A5, A8, A9, FUNCT_1:def 5, FUNCT_2:def 3;
then ( p . j <= i1 & p . j >= 1 ) by FINSEQ_1:3, NAT_1:13;
hence x in Seg i1 by A8, A9, FINSEQ_1:3; :: thesis: verum

end;

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

( p . j <= j & p . j in rng p & rng p' = Seg n ) by A6, A8, A9, FUNCT_1:def 5, FUNCT_2:def 3;
then ( p . j < i1 + 1 & p . j >= 1 ) by A10, FINSEQ_1:3, XXREAL_0:2;
then ( p . j <= i1 & p . j >= 1 ) by NAT_1:13;
hence x in Seg i1 by A8, A9, FINSEQ_1:3; :: thesis: verum

end;

end;

end;

reconsider pS = p' .: (Seg i) as finite set ;
( Seg i c= Seg n & dom p' = Seg n ) by A4, FINSEQ_1:7, FUNCT_2:67;
then Seg i,pS are_equipotent by CARD_1:60;
then ( card (Seg i) = card pS & card pS <= card (Seg i1) & card (Seg i) = i ) by A7, CARD_1:21, FINSEQ_1:78, NAT_1:44;
then i1 + 1 <= i1 by 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 )

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 A3, A4; :: thesis: verum

end;

suppose A11: 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

assume A12: for j being Nat st j in Seg n holds
p . j >= j ; :: thesis: contradiction
set NI = nat_interval i,n;
reconsider pN = p' .: (nat_interval i,n) as finite set ;
A13: 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 )
assume x in pN ; :: thesis: x in nat_interval i,n
then consider j being set such that
A14: ( j in dom p' & j in nat_interval i,n & p . j = x ) by FUNCT_1:def 12;
reconsider j = j as Nat by A14;
reconsider pj = p . j as Element of NAT by ORDINAL1:def 13;
( i <= j & j <= pj & pj in rng p' & rng p' = Seg n ) by A2, A12, A14, FUNCT_1:def 5, FUNCT_2:def 3, SGRAPH1:3;
then ( i <= pj & pj <= n ) by FINSEQ_1:3, XXREAL_0:2;
hence x in nat_interval i,n by A2, A14, SGRAPH1:2; :: thesis: verum

end;

( nat_interval i,n c= Seg n & dom p' = Seg n ) by A2, A4, FUNCT_2:67, SGRAPH1:5;
then nat_interval i,n,pN are_equipotent by CARD_1:60;
then ( card (nat_interval i,n) = card pN & i <= n ) by A4, CARD_1:21;
then ( nat_interval i,n = pN & i in nat_interval i,n ) by A2, A13, CARD_FIN:1, SGRAPH1:3;
then consider j being set such that
A15: ( j in dom p' & j in nat_interval i,n & p . j = i ) by FUNCT_1:def 12;
reconsider j = j as Nat by A15;
( j <= i & i <= j ) by A2, A12, A15, SGRAPH1:3;
hence contradiction by A11, A15, XXREAL_0:1; :: thesis: verum

end;

end;

end;