let D be set ; :: thesis: for p being one-to-one XFinSequence of D
for n being Nat holds rng (p | n) misses rng (p /^ n)
let p be one-to-one XFinSequence of D; :: thesis: for n being Nat holds rng (p | n) misses rng (p /^ n)
let n be Nat; :: thesis: rng (p | n) misses rng (p /^ n)
rng ((XFS2FS p) | n) misses rng ((XFS2FS p) /^ n) by FINSEQ_5:34;
then rng ((XFS2FS p) | n) misses rng (XFS2FS (p /^ n)) by Th17;
then rng (XFS2FS (p | n)) misses rng (XFS2FS (p /^ n)) by Th17;
then rng (XFS2FS (p | n)) misses rng (p /^ n) by AFINSQ_1:97;
hence rng (p | n) misses rng (p /^ n) by AFINSQ_1:97; :: thesis: verum