let k be Nat; :: thesis: for tr being Element of Permutations k st tr is being_transposition holds
( tr * tr = idseq k & tr = tr " )
set I = idseq k;
let tr be Element of Permutations k; :: thesis: ( tr is being_transposition implies ( tr * tr = idseq k & tr = tr " ) )
assume tr is being_transposition ; :: thesis: ( tr * tr = idseq k & tr = tr " )
then consider i, j being Nat such that
i in dom tr and
j in dom tr and
i <> j and
A1: tr . i = j and
A2: tr . j = i and
A3: for m being Nat st m <> i & m <> j & m in dom tr holds
tr . m = m ;
reconsider TR = tr as Permutation of (Seg k) by MATRIX_1:def 12;
set TT = TR * TR;
A4: dom (TR * TR) = Seg k by FUNCT_2:52;
A5: dom TR = Seg k by FUNCT_2:52;
A6: for x being object st x in dom (TR * TR) holds
(TR * TR) . x = (idseq k) . x

proof

let x be object ; :: thesis: ( x in dom (TR * TR) implies (TR * TR) . x = (idseq k) . x )
assume A7: x in dom (TR * TR) ; :: thesis: (TR * TR) . x = (idseq k) . x
reconsider m = x as Nat by A4, A7;

now :: thesis: (TR * TR) . m = m

per cases ( m = i or m = j or ( m <> i & m <> j ) ) ;

suppose ( m = i or m = j ) ; :: thesis: (TR * TR) . m = m

hence (TR * TR) . m = m by A1, A2, A7, FUNCT_1:12; :: thesis: verum

end;

suppose ( m <> i & m <> j ) ; :: thesis: (TR * TR) . m = m

then tr . m = m by A3, A4, A5, A7;
hence (TR * TR) . m = m by A7, FUNCT_1:12; :: thesis: verum

end;

end;

end;

hence (TR * TR) . x = (idseq k) . x by A4, A7, FUNCT_1:18; :: thesis: verum

end;

A8: dom (idseq k) = Seg k ;
hence tr * tr = idseq k by A6, FUNCT_1:2, FUNCT_2:52; :: thesis: tr = tr "
rng TR = Seg k by FUNCT_2:def 3;
hence tr = tr " by A4, A8, A5, A6, FUNCT_1:2, FUNCT_1:42; :: thesis: verum