set p = perm;
let q1, q2 be Element of Permutations n; :: thesis: ( ( for k being Nat st k in Seg n holds
( ( k < i implies ( ( perm . k < perm . i implies q1 . k = perm . k ) & ( perm . k >= perm . i implies q1 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies q1 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies q1 . k = (perm . (k + 1)) - 1 ) ) ) ) ) & ( for k being Nat st k in Seg n holds
( ( k < i implies ( ( perm . k < perm . i implies q2 . k = perm . k ) & ( perm . k >= perm . i implies q2 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies q2 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies q2 . k = (perm . (k + 1)) - 1 ) ) ) ) ) implies q1 = q2 )
assume that
A71: for k being Nat st k in Seg n holds
( ( k < i implies ( ( perm . k < perm . i implies q1 . k = perm . k ) & ( perm . k >= perm . i implies q1 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies q1 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies q1 . k = (perm . (k + 1)) - 1 ) ) ) ) and
A72: for k being Nat st k in Seg n holds
( ( k < i implies ( ( perm . k < perm . i implies q2 . k = perm . k ) & ( perm . k >= perm . i implies q2 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies q2 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies q2 . k = (perm . (k + 1)) - 1 ) ) ) ) ; :: thesis: q1 = q2
A73: q1 is Permutation of (Seg n) by MATRIX_1:def 12;
then A74: dom q1 = Seg n by FUNCT_2:52;
A75: now :: thesis: for x being object st x in dom q1 holds
q1 . x = q2 . x
let x be object ; :: thesis: ( x in dom q1 implies q1 . x = q2 . x )
assume A76: x in dom q1 ; :: thesis: q1 . x = q2 . x
consider k being Nat such that
A77: x = k and
1 <= k and
k <= n by A74, A76;
set k1 = k + 1;
A78: ( perm . k < perm . i or perm . k >= perm . i ) ;
A79: ( perm . (k + 1) < perm . i or perm . (k + 1) >= perm . i ) ;
( k < i or k >= i ) ;
then ( ( perm . k < perm . i & q1 . k = perm . k & q2 . k = perm . k ) or ( perm . k >= perm . i & q1 . k = (perm . k) - 1 & q2 . k = (perm . k) - 1 ) or ( perm . (k + 1) < perm . i & q1 . k = perm . (k + 1) & q2 . k = perm . (k + 1) ) or ( perm . (k + 1) >= perm . i & q1 . k = (perm . (k + 1)) - 1 & q2 . k = (perm . (k + 1)) - 1 ) ) by A71, A72, A74, A76, A77, A78, A79;
hence q1 . x = q2 . x by A77; :: thesis: verum
end;
q2 is Permutation of (Seg n) by MATRIX_1:def 12;
then dom q2 = Seg n by FUNCT_2:52;
hence q1 = q2 by A73, A75, FUNCT_1:2, FUNCT_2:52; :: thesis: verum