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_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;
now :: 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 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: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: contradiction
p .: (Seg i) c= Seg i1
proof
let x be object ; :: 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 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;
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: 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 A2, A4; :: thesis: verum
end;
suppose A22: 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 ;
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: contradiction
A25: pN c= nat_interval (i,n)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: verum
end;
end;
end;