let n be Nat; :: thesis:
let p be Element of Permutations n; :: thesis:
assume A1: p <> idseq n ; :: thesis:
reconsider p9 = p as Permutation of (Seg n) by MATRIX_1:def 12;
dom p9 = Seg n by FUNCT_2:52;
then consider x being object such that
A2: x in Seg n and
A3: p . x <> x by A1, FUNCT_1:17;
consider i being Nat such that
A4: i = x and
A5: 1 <= i and
A6: i <= n by A2;

per cases by A3, A4, XXREAL_0:1;

suppose p . i > i ; :: thesis:

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

end;

suppose A7: p . i < i ; :: thesis:

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:

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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in p .: (Seg i) ; :: thesis:
then consider y being object such that
A11: y in dom p9 and
A12: y in Seg i and
A13: p . y = x by FUNCT_1:def 6;
consider j being Nat such that
A14: j = y and
1 <= j and
A15: j <= i by A12;

per cases by A15, XXREAL_0:1;

suppose j = i ; :: thesis:

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 3;
then p . j >= 1 by A17, FINSEQ_1:1;
hence x in Seg i1 by A13, A14, A16; :: thesis:

end;

suppose A18: j < i ; :: thesis:

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 3;
then p . j >= 1 by A20, FINSEQ_1:1;
hence x in Seg i1 by A13, A14, A19; :: thesis:

end;

end;

end;

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

end;

end;

end;

end;

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

per cases by A3, A4, XXREAL_0:1;

suppose p . i < i ; :: thesis:

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

end;

suppose A22: p . i > i ; :: thesis:

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

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

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

end;

dom p9 = Seg n by FUNCT_2:52;
then nat_interval (i,n),pN are_equipotent by A5, CARD_1:33, SGRAPH1:4;
then card (nat_interval (i,n)) = card pN by CARD_1:5;
then nat_interval (i,n) = pN by A25, CARD_2:102;
then consider j being object such that
A32: j in dom p9 and
A33: j in nat_interval (i,n) and
A34: p . j = i by A23, FUNCT_1:def 6;
reconsider j = j as Nat by A33;
A35: i <= j by A33, SGRAPH1:2;
j <= i by A24, A32, A34;
hence contradiction by A22, A34, A35, XXREAL_0:1; :: thesis:

end;

end;

end;