let y be object ; :: thesis: for s being FinSequence st s " {y} <> {} holds
ex p being Permutation of (Seg (len s)) st
( (s * p) . (len s) = y & p = p " )
let s be FinSequence; :: thesis: ( s " {y} <> {} implies ex p being Permutation of (Seg (len s)) st
( (s * p) . (len s) = y & p = p " ) )
assume s " {y} <> {} ; :: thesis: ex p being Permutation of (Seg (len s)) st
( (s * p) . (len s) = y & p = p " )
then consider x being object such that
A1: x in s " {y} by XBOOLE_0:def 1;
A2: ( x in dom s & s . x in {y} ) by A1, FUNCT_1:def 7;
then A3: s . x = y by TARSKI:def 1;
A4: dom s = Seg (len s) by FINSEQ_1:def 3;
reconsider x = x as Nat by A2;

per cases ( x = len s or x <> len s ) ;

suppose A5: x = len s ; :: thesis: ex p being Permutation of (Seg (len s)) st
( (s * p) . (len s) = y & p = p " )

reconsider I = id (Seg (len s)) as Permutation of (Seg (len s)) ;
take I ; :: thesis: ( (s * I) . (len s) = y & I = I " )
x in (dom s) /\ (Seg (len s)) by A1, FUNCT_1:def 7, A4;
hence ( (s * I) . (len s) = y & I = I " ) by A5, A3, FUNCT_1:45, FUNCT_1:20; :: thesis: verum

end;

suppose A6: x <> len s ; :: thesis: ex p being Permutation of (Seg (len s)) st
( (s * p) . (len s) = y & p = p " )

( 1 <= x & x <= len s ) by A2, FINSEQ_3:25;
then A7: ( 1 <= len s & x < len s ) by A6, XXREAL_0:1, XXREAL_0:2;
then len s in dom s by FINSEQ_3:25;
then consider tr being Element of Permutations (len s) such that
A8: ( tr is being_transposition & tr . x = len s ) by A2, A4, A7, MATRIX11:16;
A9: ( tr . (len s) = x & len s in dom tr ) by A7, A8, MATRIX11:8;
reconsider tr = tr as Permutation of (Seg (len s)) by MATRIX_1:def 12;
take tr ; :: thesis: ( (s * tr) . (len s) = y & tr = tr " )
thus ( (s * tr) . (len s) = y & tr = tr " ) by A3, FUNCT_1:13, A9, A8, MATRIX11:20; :: thesis: verum

end;

end;