let n be Nat; :: thesis: for f being FinSequence st f is one-to-one & n in dom f holds

not f . n in rng (Del (f,n))

let f be FinSequence; :: thesis: ( f is one-to-one & n in dom f implies not f . n in rng (Del (f,n)) )

assume A1: f is one-to-one ; :: thesis: ( not n in dom f or not f . n in rng (Del (f,n)) )

reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

A2: dom (Del (f,n9)) c= dom f by WSIERP_1:39;

assume A3: n in dom f ; :: thesis: not f . n in rng (Del (f,n))

then consider m being Nat such that

A4: len f = m + 1 and

A5: len (Del (f,n)) = m by FINSEQ_3:104;

assume f . n in rng (Del (f,n)) ; :: thesis: contradiction

then consider j being object such that

A6: j in dom (Del (f,n)) and

A7: f . n = (Del (f,n)) . j by FUNCT_1:def 3;

A8: j in Seg m by A5, A6, FINSEQ_1:def 3;

reconsider j = j as Element of NAT by A6;

not f . n in rng (Del (f,n))

let f be FinSequence; :: thesis: ( f is one-to-one & n in dom f implies not f . n in rng (Del (f,n)) )

assume A1: f is one-to-one ; :: thesis: ( not n in dom f or not f . n in rng (Del (f,n)) )

reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

A2: dom (Del (f,n9)) c= dom f by WSIERP_1:39;

assume A3: n in dom f ; :: thesis: not f . n in rng (Del (f,n))

then consider m being Nat such that

A4: len f = m + 1 and

A5: len (Del (f,n)) = m by FINSEQ_3:104;

assume f . n in rng (Del (f,n)) ; :: thesis: contradiction

then consider j being object such that

A6: j in dom (Del (f,n)) and

A7: f . n = (Del (f,n)) . j by FUNCT_1:def 3;

A8: j in Seg m by A5, A6, FINSEQ_1:def 3;

reconsider j = j as Element of NAT by A6;

per cases
( j < n9 or j >= n9 )
;

end;

suppose A9:
j < n9
; :: thesis: contradiction

then
f . n = f . j
by A7, FINSEQ_3:110;

hence contradiction by A1, A3, A6, A2, A9, FUNCT_1:def 4; :: thesis: verum

end;hence contradiction by A1, A3, A6, A2, A9, FUNCT_1:def 4; :: thesis: verum

suppose A10:
j >= n9
; :: thesis: contradiction

A11:
j + 1 >= 0 + 1
by XREAL_1:6;

A12: j <= m by A8, FINSEQ_1:1;

then j + 1 <= m + 1 by XREAL_1:6;

then j + 1 in Seg (m + 1) by A11;

then A13: j + 1 in dom f by A4, FINSEQ_1:def 3;

A14: j + 1 <> n by A10, NAT_1:13;

f . n = f . (j + 1) by A3, A4, A7, A10, A12, FINSEQ_3:111;

hence contradiction by A1, A3, A13, A14, FUNCT_1:def 4; :: thesis: verum

end;A12: j <= m by A8, FINSEQ_1:1;

then j + 1 <= m + 1 by XREAL_1:6;

then j + 1 in Seg (m + 1) by A11;

then A13: j + 1 in dom f by A4, FINSEQ_1:def 3;

A14: j + 1 <> n by A10, NAT_1:13;

f . n = f . (j + 1) by A3, A4, A7, A10, A12, FINSEQ_3:111;

hence contradiction by A1, A3, A13, A14, FUNCT_1:def 4; :: thesis: verum