let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st p in rng f & f is one-to-one holds
f :- p is one-to-one
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & f is one-to-one holds
f :- p is one-to-one
let f be FinSequence of D; :: thesis: ( p in rng f & f is one-to-one implies f :- p is one-to-one )
assume p in rng f ; :: thesis: ( not f is one-to-one or f :- p is one-to-one )
then ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i ) by Th49;
hence ( not f is one-to-one or f :- p is one-to-one ) ; :: thesis: verum