let n be Nat; 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; ( 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
; ( 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_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;
hence
ex j being Nat st
( j in Seg n & p . j > j )
; 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 A22:
p . i > i
;
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 )
verumproof
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
;
contradiction
A25:
pN c= nat_interval (
i,
n)
proof
let x be
object ;
TARSKI:def 3 ( not x in pN or x in nat_interval (i,n) )
A26:
rng p9 = Seg n
by FUNCT_2:def 3;
assume
x in pN
;
x in nat_interval (i,n)
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;
verum
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;
verum
end; end; end;