let p be FinSequence; :: thesis: for x being set st x in rng p & p is one-to-one holds
p - {x} = (p -| x) ^ (p |-- x)
let x be set ; :: 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 Th10;
hence p - {x} = (p -| x) ^ (p |-- x) by Th69; :: thesis: verum