let p be FinSequence; :: thesis: for x being object st x in rng p & p is one-to-one holds
p |-- x is one-to-one
let x be object ; :: thesis: ( x in rng p & p is one-to-one implies p |-- x is one-to-one )
assume x in rng p ; :: thesis: ( not p is one-to-one or p |-- x is one-to-one )
then p = ((p -| x) ^ <*x*>) ^ (p |-- x) by Th51;
hence ( not p is one-to-one or p |-- x is one-to-one ) by FINSEQ_3:91; :: thesis: verum