let p be FinSequence; 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 ; ( x in rng p & p is one-to-one implies p -| x is one-to-one )
assume
x in rng p
; ( not p is one-to-one or p -| x is one-to-one )
then p =
((p -| x) ^ <*x*>) ^ (p |-- x)
by Th51
.=
(p -| x) ^ (<*x*> ^ (p |-- x))
by FINSEQ_1:32
;
hence
( not p is one-to-one or p -| x is one-to-one )
by FINSEQ_3:91; verum