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

proof

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

now

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 A2, A5, FUNCT_1:22; :: thesis: verum

end;

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

then ( tr . m <> i & tr . m <> j & tr . m = m ) by A3, A4, A5;
hence (TR * TR) . m = m by A5, FUNCT_1:22; :: thesis: verum

end;

end;

end;

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

end;

hence A6: tr * tr = idseq k by A4, FUNCT_1:9; :: thesis: tr = tr "
rng TR = Seg k by FUNCT_2:def 3;
hence tr = tr " by A4, A6, FUNCT_1:64; :: thesis: verum