let p be FinSequence; :: thesis: for x being object st x in rng p & p is one-to-one holds
rng (p -| x) misses rng (p |-- x)
let x be object ; :: thesis: ( x in rng p & p is one-to-one implies rng (p -| x) misses rng (p |-- x) )
assume that
A1: x in rng p and
A2: p is one-to-one ; :: thesis: rng (p -| x) misses rng (p |-- x)
p = ((p -| x) ^ <*x*>) ^ (p |-- x) by A1, Th51;
then rng (p |-- x) misses rng ((p -| x) ^ <*x*>) by A2, FINSEQ_3:91;
hence rng (p -| x) misses rng (p |-- x) by FINSEQ_1:29, XBOOLE_1:63; :: thesis: verum