let p be Permutation of (Seg 3); :: thesis: ( p = <*3,2,1*> implies p is being_transposition )
assume A1: p = <*3,2,1*> ; :: thesis:
then A2: dom p = {1,2,3} by ;
ex i, j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) )
proof
take i = 1; :: thesis: ex j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) )

take j = 3; :: thesis: ( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) )

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

for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k
proof
let k be Nat; :: thesis: ( k <> i & k <> j & k in dom p implies p . k = k )
assume ( k <> i & k <> j & k in dom p ) ; :: thesis: p . k = k
then k = 2 by ;
hence p . k = k by ; :: thesis: verum
end;
hence ( i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) ) by ; :: thesis: verum
end;
hence p is being_transposition by MATRIX_1:def 14; :: thesis: verum