let p be FinSequence; :: thesis: for k being set st k in dom p holds
len p > 0
let k be set ; :: thesis: ( k in dom p implies len p > 0 )
assume k in dom p ; :: thesis: len p > 0
then p <> {} ;
hence len p > 0 ; :: thesis: verum