let n be Nat; :: thesis: for P being Permutation of Seg n st P is being_transposition holds
for i, j being Nat st i < j holds
( P . i = j iff ( i in dom P & j in dom P & P . i = j & P . j = i & ( for k being Nat st k <> i & k <> j & k in dom P holds
P . k = k ) ) )
let P be Permutation of Seg n; :: thesis: ( P is being_transposition implies for i, j being Nat st i < j holds
( P . i = j iff ( i in dom P & j in dom P & P . i = j & P . j = i & ( for k being Nat st k <> i & k <> j & k in dom P holds
P . k = k ) ) ) )
assume A1: P is being_transposition ; :: thesis: for i, j being Nat st i < j holds
( P . i = j iff ( i in dom P & j in dom P & P . i = j & P . j = i & ( for k being Nat st k <> i & k <> j & k in dom P holds
P . k = k ) ) )
let i, j be Nat; :: thesis: ( i < j implies ( P . i = j iff ( i in dom P & j in dom P & P . i = j & P . j = i & ( for k being Nat st k <> i & k <> j & k in dom P holds
P . k = k ) ) ) )
assume A2: i < j ; :: thesis: ( P . i = j iff ( i in dom P & j in dom P & P . i = j & P . j = i & ( for k being Nat st k <> i & k <> j & k in dom P holds
P . k = k ) ) )
consider i', j' being Nat such that
( i' in dom P & j' in dom P ) and
A3: ( i' <> j' & P . i' = j' & P . j' = i' ) and
A4: for k being Nat st k <> i' & k <> j' & k in dom P holds
P . k = k by A1, MATRIX_2:def 14;
thus ( P . i = j implies ( i in dom P & j in dom P & P . i = j & P . j = i & ( for k being Nat st k <> i & k <> j & k in dom P holds
P . k = k ) ) ) :: thesis: ( i in dom P & j in dom P & P . i = j & P . j = i & ( for k being Nat st k <> i & k <> j & k in dom P holds
P . k = k ) implies P . i = j )

proof

assume A5: P . i = j ; :: thesis: ( i in dom P & j in dom P & P . i = j & P . j = i & ( for k being Nat st k <> i & k <> j & k in dom P holds
P . k = k ) )
then A6: i in dom P by A2, FUNCT_1:def 4;
then A7: ( P . i in rng P & rng P = Seg n & dom P = Seg n ) by FUNCT_1:def 5, FUNCT_2:67, FUNCT_2:def 3;
then P . j <> j by A2, A5, A6, FUNCT_1:def 8;
then ( ( j = j' or j = i' ) & ( i = j' or i = i' ) ) by A4, A5, A6, A7;
hence ( i in dom P & j in dom P & P . i = j & P . j = i & ( for k being Nat st k <> i & k <> j & k in dom P holds
P . k = k ) ) by A3, A4, A5, A7, FUNCT_1:def 5; :: thesis: verum

end;

thus ( i in dom P & j in dom P & P . i = j & P . j = i & ( for k being Nat st k <> i & k <> j & k in dom P holds
P . k = k ) implies P . i = j ) ; :: thesis: verum