let k be Nat; :: thesis: for y being object
for s being FinSequence st card (s " {y}) = k holds
ex p being Permutation of (dom s) ex s1 being FinSequence st
( s * p = s1 ^ (k |-> y) & not y in rng s1 )
let y be object ; :: thesis: for s being FinSequence st card (s " {y}) = k holds
ex p being Permutation of (dom s) ex s1 being FinSequence st
( s * p = s1 ^ (k |-> y) & not y in rng s1 )
let s be FinSequence; :: thesis: ( card (s " {y}) = k implies ex p being Permutation of (dom s) ex s1 being FinSequence st
( s * p = s1 ^ (k |-> y) & not y in rng s1 ) )
assume A1: card (s " {y}) = k ; :: thesis: ex p being Permutation of (dom s) ex s1 being FinSequence st
( s * p = s1 ^ (k |-> y) & not y in rng s1 )

per cases ( k = 0 or k <> 0 ) ;

suppose A2: k = 0 ; :: thesis: ex p being Permutation of (dom s) ex s1 being FinSequence st
( s * p = s1 ^ (k |-> y) & not y in rng s1 )

take p = id (dom s); :: thesis: ex s1 being FinSequence st
( s * p = s1 ^ (k |-> y) & not y in rng s1 )
take s ; :: thesis: ( s * p = s ^ (k |-> y) & not y in rng s )
( s * p = s & k |-> y = {} ) by A2, RELAT_1:52;
hence s * p = s ^ (k |-> y) ; :: thesis: not y in rng s
assume y in rng s ; :: thesis: contradiction
then consider x being object such that
A3: ( x in dom s & s . x = y ) by FUNCT_1:def 3;
s . x in {y} by A3, TARSKI:def 1;
then x in s " {y} by A3, FUNCT_1:def 7;
hence contradiction by A2, A1; :: thesis: verum

end;

suppose k <> 0 ; :: thesis: ex p being Permutation of (dom s) ex s1 being FinSequence st
( s * p = s1 ^ (k |-> y) & not y in rng s1 )

then not s " {y} is empty by A1;
then consider x being object such that
A4: x in s " {y} ;
( x in dom s & s . x in {y} ) by A4, FUNCT_1:def 7;
then ( y = s . x & s . x in rng s ) by FUNCT_1:def 3, TARSKI:def 1;
then reconsider L = {y} as Subset of (rng s) by ZFMISC_1:31;
(L `) ` = L ;
then consider p being Permutation of (dom s) such that
A5: (s - L) ^ (s - (L `)) = s * p by FINSEQ_3:115;
take p ; :: thesis: ex s1 being FinSequence st
( s * p = s1 ^ (k |-> y) & not y in rng s1 )
take s1 = s - L; :: thesis: ( s * p = s1 ^ (k |-> y) & not y in rng s1 )
L ` = (rng s) \ L by SUBSET_1:def 4;
then s " (L `) = (s " (rng s)) \ (s " L) by FUNCT_1:69;
then s " (L `) = (dom s) \ (s " L) by RELAT_1:134;
then card (s " (L `)) = (card (dom s)) - (card (s " L)) by RELAT_1:132, CARD_2:44;
then card (s " (L `)) = (card (Seg (len s))) - (card (s " L)) by FINSEQ_1:def 3;
then A6: len (s - (L `)) = (len s) - ((len s) - k) by A1, FINSEQ_3:59;
rng (s - (L `)) = (rng s) \ (L `) by FINSEQ_3:65
.= (rng s) \ ((rng s) \ L) by SUBSET_1:def 4
.= (rng s) /\ L by XBOOLE_1:48
.= L by XBOOLE_1:28 ;
then s - (L `) = (dom (s - (L `))) --> y by FUNCOP_1:9;
hence s * p = s1 ^ (k |-> y) by A5, A6, FINSEQ_1:def 3; :: thesis: not y in rng s1
( rng (s - L) = (rng s) \ L & y in {y} ) by FINSEQ_3:65, TARSKI:def 1;
hence not y in rng s1 by XBOOLE_0:def 5; :: thesis: verum

end;

end;