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 i9, j9 being Nat such that
i9 in dom P and
j9 in dom P and
i9 <> j9 and
A1: P . i9 = j9 and
A2: P . j9 = i9 and
A3: for k being Nat st k <> i9 & k <> j9 & 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 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:52;
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 2;
then ( i = j9 or i = i9 ) 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 3; :: 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