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
A43: 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
A44: 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
( q1 is Permutation of (Seg n) & q2 is Permutation of (Seg n) ) by MATRIX_2:def 11;
then A45: ( dom q1 = Seg n & dom q2 = Seg n ) by FUNCT_2:67;

now

let x be set ; :: thesis: ( x in dom q1 implies q1 . x = q2 . x )
assume A46: x in dom q1 ; :: thesis: q1 . x = q2 . x
consider k being Element of NAT such that
A47: ( x = k & 1 <= k & k <= n ) by A45, A46;
set k1 = k + 1;
( ( k < i or k >= i ) & ( perm . k < perm . i or perm . k >= perm . i ) & ( perm . (k + 1) < perm . i or perm . (k + 1) >= perm . 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 A43, A44, A45, A46, A47;
hence q1 . x = q2 . x by A47; :: thesis: verum

end;

hence q1 = q2 by A45, FUNCT_1:9; :: thesis: verum