let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st p in rng f holds
not f -: p is empty
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds
not f -: p is empty
let f be FinSequence of D; :: thesis: ( p in rng f implies not f -: p is empty )
assume A1: p in rng f ; :: thesis: not f -: p is empty
then 1 <= p .. f by FINSEQ_4:21;
then 1 <= len (f -: p) by A1, Th42;
hence not f -: p is empty ; :: thesis: verum