let z be FinSequence; :: thesis: for i being Nat st z is_one-to-one_at i holds
rng (Del (z,i)) = (rng z) \ {(z . i)}
let i be Nat; :: thesis: ( z is_one-to-one_at i implies rng (Del (z,i)) = (rng z) \ {(z . i)} )
assume A1: z is_one-to-one_at i ; :: thesis: rng (Del (z,i)) = (rng z) \ {(z . i)}
not z . i in rng (Del (z,i))

proof

assume z . i in rng (Del (z,i)) ; :: thesis: contradiction
then consider x being object such that
A2: ( x in dom (Del (z,i)) & (Del (z,i)) . x = z . i ) by FUNCT_1:def 3;
reconsider x = x as Nat by A2;
A3: i in dom z by A1, FINSEQ_4:3;
then A4: len z = (len (Del (z,i))) + 1 by WSIERP_1:def 1;
A5: ( 1 <= x & x <= len (Del (z,i)) ) by A2, FINSEQ_3:25;
then A6: x < len z by A4, NAT_1:13;
then ( 1 <= x + 1 & x + 1 <= len z ) by NAT_1:11, NAT_1:13;
then A7: ( x in dom z & x + 1 in dom z ) by A5, A6, FINSEQ_3:25;

per cases ( x < i or x >= i ) ;

suppose A8: x < i ; :: thesis: contradiction

then (Del (z,i)) . x = z . x by A3, WSIERP_1:def 1;
hence contradiction by A8, A1, A2, A7, FINSEQ_4:3; :: thesis: verum

end;

suppose A9: x >= i ; :: thesis: contradiction

then (Del (z,i)) . x = z . (x + 1) by A3, WSIERP_1:def 1;
then x + 1 = i by A1, A2, A7, FINSEQ_4:3;
hence contradiction by A9, NAT_1:13; :: thesis: verum

end;

end;

end;

then A10: rng (Del (z,i)) c= (rng z) \ {(z . i)} by FINSEQ_3:106, ZFMISC_1:34;
(rng z) \ {(z . i)} c= rng (Del (z,i))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (rng z) \ {(z . i)} or y in rng (Del (z,i)) )
assume A11: y in (rng z) \ {(z . i)} ; :: thesis: y in rng (Del (z,i))
consider x being object such that
A12: ( x in dom z & z . x = y ) by A11, FUNCT_1:def 3;
reconsider x = x as Nat by A12;
A13: i in dom z by A1, FINSEQ_4:3;
then A14: len z = (len (Del (z,i))) + 1 by WSIERP_1:def 1;
A15: ( 1 <= x & x <= len z ) by A12, FINSEQ_3:25;
A16: ( 1 <= i & i <= len z ) by A13, FINSEQ_3:25;
x <> i by A11, ZFMISC_1:56, A12;

per cases then ( x < i or x > i ) by XXREAL_0:1;

suppose A17: x < i ; :: thesis: y in rng (Del (z,i))

then x < len z by A16, XXREAL_0:2;
then x <= len (Del (z,i)) by A14, NAT_1:13;
then A18: x in dom (Del (z,i)) by A15, FINSEQ_3:25;
(Del (z,i)) . x = z . x by A17, A13, WSIERP_1:def 1;
hence y in rng (Del (z,i)) by A12, A18, FUNCT_1:def 3; :: thesis: verum

end;

suppose A19: x > i ; :: thesis: y in rng (Del (z,i))

then reconsider x1 = x - 1 as Nat ;
x1 + 1 > i by A19;
then A20: x1 >= i by NAT_1:13;
then A21: x1 >= 1 by A16, XXREAL_0:2;
x1 + 1 <= (len (Del (z,i))) + 1 by A13, A15, WSIERP_1:def 1;
then x1 <= len (Del (z,i)) by XREAL_1:6;
then A22: x1 in dom (Del (z,i)) by A21, FINSEQ_3:25;
(Del (z,i)) . x1 = z . (x1 + 1) by A13, A20, WSIERP_1:def 1;
hence y in rng (Del (z,i)) by A12, A22, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

hence rng (Del (z,i)) = (rng z) \ {(z . i)} by A10, XBOOLE_0:def 10; :: thesis: verum