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 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 ) ) )
then consider i', j' being Nat such that
i' in dom P and
j' in dom P and
i' <> j' and
A1: P . i' = j' and
A2: P . j' = i' and
A3: for k being Nat st k <> i' & k <> j' & k in dom P holds
P . k = k by MATRIX_2:def 14;
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 A4: 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 ) ) )
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

A5: dom P = Seg n by FUNCT_2:67;
A6: rng P = Seg n by FUNCT_2:def 3;
assume A7: 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 A8: i in dom P by A4, FUNCT_1:def 4;
then ( i = j' or i = i' ) by A4, A3, 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 A1, A2, A3, A7, A8, A6, A5, 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