let n be Nat; for f being FinSequence st f is one-to-one holds
rng (f | n) misses rng (f /^ n)
let f be FinSequence; ( f is one-to-one implies rng (f | n) misses rng (f /^ n) )
assume A1:
f is one-to-one
; rng (f | n) misses rng (f /^ n)
A2:
dom (f | n) c= dom f
by Th18;
assume
rng (f | n) meets rng (f /^ n)
; contradiction
then consider x being object such that
A3:
x in rng (f | n)
and
A4:
x in rng (f /^ n)
by XBOOLE_0:3;
consider i being object such that
A5:
i in dom (f | n)
and
A6:
(f | n) . i = x
by A3, FUNCT_1:def 3;
consider j being object such that
A7:
j in dom (f /^ n)
and
A8:
(f /^ n) . j = x
by A4, FUNCT_1:def 3;
reconsider ii = i, jj = j as Nat by A7, A5;
A9:
jj + n in dom f
by A7, Th26;
A10:
now not ii = jj + nend;
f . (jj + n) =
(f /^ n) . j
by A7, Th27
.=
f . i
by A5, FUNCT_1:47, A6, A8
;
hence
contradiction
by A1, A5, A2, A9, A10; verum