let f be FinSequence; :: thesis: for p, q being set st p in rng f & q in rng f & p .. f = q .. f holds
p = q
let p, q be set ; :: thesis: ( p in rng f & q in rng f & p .. f = q .. f implies p = q )
assume that
A1: p in rng f and
A2: q in rng f ; :: thesis: ( not p .. f = q .. f or p = q )
assume p .. f = q .. f ; :: thesis: p = q
hence p = f . (q .. f) by A1, FINSEQ_4:19
.= q by A2, FINSEQ_4:19 ;
:: thesis: verum