let p be FinSequence; :: thesis: for x being object st x in rng p & p is one-to-one holds
p - {x} = (p -| x) ^ (p |-- x)
let x be object ; :: thesis: ( x in rng p & p is one-to-one implies p - {x} = (p -| x) ^ (p |-- x) )
assume ( x in rng p & p is one-to-one ) ; :: thesis: p - {x} = (p -| x) ^ (p |-- x)
then p just_once_values x by Th8;
hence p - {x} = (p -| x) ^ (p |-- x) by Th54; :: thesis: verum